doubt in CTL

Question

The final answer for this is {s0...s6}
should we consider S0 for solving the given equation ? As it is an unreachable state I thought we should not consider it.

Answer 1

Good question. However, as the exam problem is asking which states satisfy the property, we have to consider all the state of the structure even though s0 is not reachable. Note also that model checking might be used to check whether a state is reachable, and then we definitely have to evaluate the formula for reachable states in all the states.