# Given two formulae E[G F p] (which is CTL*) and EG EF p ( which is a CTL) with a Model prove that they are not equivalent

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.

• 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. Dec 2 '17 at 12:41
• @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. 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.