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
