Why is GFp -> GFq false in LTL, even though GFp and GFq are false?

Consider the Kripke structure: $$\begin{array}{ccccccc} \to & (p, \neg q) & \to & (\neg p, \neg q) & \to & (\neg p, q) \\ & \circlearrowright & & \circlearrowright & & \circlearrowright & \\ \end{array}$$

where $(p, \neg q)$ means “$p$ and not $q$” and $\circlearrowright$ is a self loop. We number the states $s_1, s_2, s_3$ from left to right. Now consider the three LTL properties: $$\begin{array}{ll} M \vDash \mathbf{G}\,\mathbf{F}\,p \to \mathbf{G}\,\mathbf{F}\,q & \text{false} \\ M \vDash \mathbf{G}\,\mathbf{F}\,p & \text{false} \\ M \vDash \mathbf{G}\,\mathbf{F}\,q & \text{false} \\ \end{array}$$

The oddity is this: how can $\text{false} \to \text{false}$ be false?

P.S.: I am sure of the results because I used NuSMV with the following code:

MODULE main
VAR
state : {a, b, c};
p : boolean;
q : boolean;

ASSIGN
init(state) := a;
next(state) :=
case
state=a : {a,b};
state=b : c;
state=c : c;
esac;
p :=
case
state=a : TRUE;
state=b : FALSE;
state=c : FALSE;
esac;
q :=
case
state=a : FALSE;
state=b : FALSE;
state=c : TRUE;
esac;

LTLSPEC
((G ( F p = TRUE)) ->  (G ( F q = TRUE)))
LTLSPEC
(G ( F p = TRUE))
LTLSPEC
(G ( F q = TRUE))


This happens because of the way LTL formulae are evaluated over Kripke structures: Recall that LTL is first of all a logic of traces; when we say that a Kripke structure $S$ satisfies $\varphi$, we mean that all its traces do, i.e. we have an implicit universal quantification.

The consequence is that, for an LTL formula $\varphi$, it is possible that neither $\varphi$ nor $\neg\varphi$ is true for $S$, because neither holds for all traces. Similarly, none of your three formulas above holds for every trace.

If you are more familiar with predicate calculus, this is just saying that $(\forall x.A)\vee(\forall x.\neg A)$ is not a tautology, and neither is $(\forall x.A)\vee(\forall x.B)\vee(\forall x.A\to B)$.

Extending upon Klaus' answer, here are counter-examples:

1. $s_1^\omega = (p,\lnot q)^\omega$ is a trace -- so $\mathrm{G}\, \mathrm{F}\, q$ is not valid.
2. $s_1s_2^\omega = (p,\lnot q)(\lnot p,\lnot q)^\omega$ is a trace -- so $\mathrm{G}\, \mathrm{F}\, p$ is not valid.
3. $s_1^\omega = (p,\lnot q)^\omega$ is a trace -- $\mathrm{G}\, \mathrm{F}\, p$ holds for this trace but $\mathrm{G}\, \mathrm{F}\, q$ does not, so $\mathrm{G}\, \mathrm{F}\, p \to \mathrm{G}\, \mathrm{F}\, q$ is not valid, either.

Your intuition might have mislead you, saying that "$M \models \phi$ false" meant that $\phi$ did never hold (in $M$), that is "$M \models \lnot \phi$ true". This is not true and is not as odd as you might think. The effect is not restricted to LTL: in all logics you can have formulae which are not valid (that is, are no tautologies), nor are their respective negations (not that you had a negation in your example), nor are implications of them. Just consider $a \lor b$ and $\lnot a \land \lnot b$ in propositional logic.

However shouldn't the trace $s_1^w$ be more instructive for your reasons? in this trace $\mathrm{G}\,\mathrm{F}\,p$ holds always however $\mathrm{G}\,\mathrm{F}\,q$ doesn't, therefore $\mathrm{G}\,\mathrm{F}\,p \to\mathrm{G}\,\mathrm{F}\,p$ becomes false.

• Oh, my example 3. was wrong; this is a correct counter example. Thanks! Was this intended to be a comment? – Raphael Jul 4 '12 at 8:00
• yes but it didn't let me reply so had to post as new line.. – user9948 Jul 4 '12 at 13:06