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

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?

(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$$.