# Equivalence of GFp and Gp in LTL

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?

## 1 Answer

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.