distinguishing between CTL* formulas $A[FG p]$ and $AFAG p$ using transition system
(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 ----&gt; q1 ----&gt; 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$.