Computation tree logic and Kripke structures

Question

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?

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.