# Temporal logic CTL model checking

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.

+1 vote

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).
by (147k points)
edited by