# Computation tree logic and Kripke structures

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?

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.