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?


1 Answer 1


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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.