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.
$\begingroup$
$\endgroup$
2
-
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$– ShaullCommented 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$– noobAtWorkCommented Dec 2, 2017 at 12:50
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
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.
