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 "If p is true in every reachable state, then for any path along which q is continuously true, r becomes true" is a far
cry from the meaning of the formula above.
The premise "p is true in every reachable state" can be modeled by
AG(p). The conclusion "for any path along which q is continuously true, r becomes true" may be expressed by the CTL* formula
A(G q F r).
Thus, the English language specification is modeled by the
CTL* formula
AG(p) A(G p F r). Note that this has
a completely different meaning than
AG(p A[q U r]).
For example, consider a state s in a model where each state t, reachable
from s, satisfies p. Then the former formula insists that all computation
paths beginning in s, on which q is true globally, to reach a state in which r is true.
The latter formula, however,
insists on A[q U r] to hold at all reachable states t, for p holds for
all of them, thereby "triggering" the implication!
(Can you express A(G q F r)
in CTL?)
Back to Question.
Next Question.