[Solved]: Computation tree logic and Kripke structures

Problem Detail: 

Specifications in Kripke structures are verified by Computation tree logic (CTL). However, refering to this Wikipedia article the CTL-operators are relative to a current state. So, when we want to verify if EF q is satisfied in a Kripke structure

Do we only need to check if EF q holds starting from the starting state oder do we need to check if EF q holds starting from every state?

Asked By : 0xbadf00d

Answered By : Shaull

CTL formulas are always evaluated from the starting state of the Kripke structure. Indeed, CTL stands for computation Tree logic, and the tree in question is the unwinding of the Kripke structure, starting from the initial state.

If you want to specify that $EF q$ should hold from every (reachable) state, that can be specified as $AGEFq$, which is still a CTL formula.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/20191

3.2K people like this

 Download Related Notes/Documents