distinguishing between CTL* formulas $A[FG p]$ and $AFAG p$ using transition system

Question

It is to show, using a transition system, that the two formulas $A[FG p]$ and $AFAG p$ are not equivalent.

For me, it seems strange that they are not equivalent.

As the first one says that any computation path eventually has $p$ always true.

And the second one says that any computation path contains a state such that any path starting at this state has $p$ always true.

Aren't they equivalent?

Answer 1

(This is the "standard" example which proves that CTL is not a superset of LTL, in terms of expressiveness)

Consider this system:

• state $q0$, transitions to $q0$ and $q1$
• state $q1$, transition to $q2$
• state $q2$, transition to $q2$

Let $p$ be true in $q0,q2$ but not in $q1$.

(p)     (not p)    (p)
 q0 ----> q1 ----> q2
| ^               | ^
\-/               \-/

State $q0$ does not satisfy formula $AF[AGp]$. Take the infinite path $q0,q0,q0,\ldots$. There is no state in the path satisfying $AGp$ since we can only pick $q0$ and from there the path $q0,q1,q2,q2,q2,\ldots$ does not satisfy $Gp$ since $q1$ does not satisfy $p$.

State $q0$ however satisfies $A[FGp]$. Take any infinite path starting from $q0$. Either it is of the form $q0,q0,q0,\ldots$ or of the form $q0,q0,q0,\ldots,q0,q1,q2,q2,q2,\ldots$. Both forms satisfy $FGp$.