3
$\begingroup$

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))
$\endgroup$
5
$\begingroup$

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)$.

$\endgroup$
3
$\begingroup$

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.

$\endgroup$
0
$\begingroup$

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.

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.