I am trying to prove they are not equivalent , a model which satisfies the fist one but not the second since I think EG EF p is stronger than E[GF p],any leads would be helpful. Thanks.

  • 1
    $\begingroup$ Which models have you tried? Perhaps try to translate those formulas to English, and see if you can extract a model from that. Hint: 3 states should suffice. $\endgroup$
    – Shaull
    Commented Dec 2, 2017 at 12:41
  • $\begingroup$ @Shauli ok.. so first one says " there exist a path where p occurs infinitely often " and the second one says " there is a path in which what ever state i am in (EG) I will be having a path with p in the future(EF). There is a subtle thing which I am missing which I don't know. $\endgroup$
    – noobAtWork
    Commented Dec 2, 2017 at 12:50

1 Answer 1


Consider a system with 3 states, $s_1,s_2,s_3$ and the following transitions: $s_1\to s_1$, $s_1\to s_2$, $s_2\to s_3$ and $s_3\to s_3$.

The state $s_2$ is labelled $p$.

Clearly $E[GF p]$ doesn't hold, since every path from $s_1$ has at most one $p$.

However, there exists a path, namely $s_1^\omega$, such that in every state along this path, i.e. in $s_1$, there exists a path that eventually sees $p$, so $E G EF p$ does hold.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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