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
    Dec 2 '17 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
    Dec 2 '17 at 12:50

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, privacy policy and cookie policy

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