0
$\begingroup$

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?

$\endgroup$
1
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.