Temporal logic CTL model checking

Question

Q c) Compute the set of states satisfy 

S2=A G (a&b)

I tried to solve this question as below :

Set of state satisfy a is {s4}

Set of states satisfy b are {s1,s2,s3,s5,s6}

Set of states satisfy the conjunction of a & b is {} 

Now, at this point I am confused why A G ({}) is {s4} ?, as there is no path from initial states to s4 and s4 is an unreachable state.

Answer 1

AG phi holds on a state if and only if all infinite paths leaving s satisfy phi. States (like s4 in the example) that do not have any infinite outgoing paths, therefore satisfy any CTL* formula starting with an A quantifier, so even A G false (as in your case) is true in such states.

For many people, this appears to be quite non-intuitive. Therefore, we had the discussion about eliminating all states without infinite paths (remember the exercises and discussions about Kripke structures and FSMs).

Comments

Thanks for your answer.