Correct Answer.
AG(p 
AG(p 
q)) being true at s0 means that at any state t reachable from s0 (the "AG"), where p is true (the "p ..."), the formula
AG(p q) is true at state t.
- All four states of this model are reachable from s0.
- However, p is true only at the states s1 and s3.
- Therefore, it suffices to check (why?) whether
AG(p q) holds at the states s1 and s3.
- The formula AG(p q) is true
at s1 and s3 if p q is true at every state reachable from s1 and s3,
respectively. The states s1, s2 and s3 are
the ones that are reachable from s1 and s3, and these all satisfy p q. Therefore,
AG(p q) is true at s1 and s3.
- In summary,
AG(p AG(p q)) is true at s0.
Back to Question.
Next Question.