Incorrect Answer.
We determine the meaning of the CTL formula AG (p 
A[q U r]) by
- breaking it up into significant subformulas,
- determining the meaning of these subformulas, and by
- determining the meaning of the entire formula by composing the meanings
of subformulas in the manner suggested by the logic operators
that are present.
To wit,
- the meaning of A[q U r] at any state s is that 'for all computation paths
that begin in s, the predicate q is true until the path reaches a state in
which r is true (and such a state has to be reached)'.
- The meaning of p A[q U r] at
any state s is that 'if p holds in state s, then A[q U r] has to hold at
state s as well'.
- The meaning of AG(p A[q U r]) at
any state s is that 'p A[q U r] holds
at any state t that is reachable from state s'.
The English specification "Any reachable state in which p is true has a path
from it on which r is eventually true, and until then q is true" comes pretty
close to being modeled by the formula above. However, there is a crucial
difference. While both talk about reachable states and a conditional
guaratee for such states in terms of the condition p, the former guarantees that "q U r" is satisfied for
all computation paths from such states, whereas the latter
only insists on the existence of such a path.
In light of this, we infer that the English specification is adequately
modeled by the CTl formula
AG(p E[q U r])
instead of AG(p A[q U r]).
Back to Question.
Next Question.