Correct Answer.
AG(p 
AF(p 
r)) being true at s0 means that at any state t reachable from
s0 (the "AG"), where p is true (the "p ..."), the formula AF(p r) has
to be true at state t.
- All four states of the model are reachable from s0.
- But p is true only at s1 and s3.
- Therefore, we only have to check AF(p r) at the states s1 and s3.
- All paths from s1 and s3 eventually reach the state
s1, where p r is true.
So AF(p r) is true at s1 and s3.
- Hence AG(p AF(p r)) is true at s0.
Back to Question.
Next Question.