patternMinor
Equivalence of GFp and Gp in LTL
Viewed 0 times
andgfpequivalenceltl
Problem
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?
$\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?
Solution
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.
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.
Context
StackExchange Computer Science Q#6532, answer score: 5
Revisions (0)
No revisions yet.