Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

1k questions

1.2k answers


498 users

0 votes

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.
in * TF "Emb. Sys. and Rob." by (2.9k points)

1 Answer

+1 vote
Best answer
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 (162k points)
edited by
Thanks for your answer.

Related questions

0 votes
1 answer
asked Feb 14, 2021 in * TF "Emb. Sys. and Rob." by daodubasit (790 points)
0 votes
1 answer
0 votes
1 answer
0 votes
2 answers
Imprint | Privacy Policy