[Solved]: Equivalence of GFp and Gp in LTL

Problem Detail: 

In linear time logic, is $\mathbf{GF}p$ equivalent to $ \mathbf{G}p$ ?

$\mathbf{GF}p$ means that it is always the case that p is true eventually.

Let $\mathbf{G} p$ be defined as: $\forall j \ge0,\ p$ holds in the suffix $q_j, q_{j+1}, q_{j+2},\ldots$

and since: formula $φ$ holds for state machine $M$ if $φ$ holds for all possible traces of $M$

Isn't $\mathbf{G}$ in $\mathbf{GF}p$ redundant then?

Asked By : prasopes

Answered By : Pål GD

No, not equivalent and not redundant.

Consider $p$ being true if and only if $j$ is even. $\mathbf{G}p$ is not true (obviously, since $p$ is false in every odd state), but $\mathbf{GF}p$ is always true.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/6532

 Ask a Question

 Download Related Notes/Documents