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?