# Validity of LTL formulas in a given transition system

Say I have the following transition system:

I've understood how I can tell if □a and ⟡b are valid (□a is invalid because a is not true is S2 and ⟡b is valid there is a state (i.e. S1) in which b is true. Please correct me if I'm wrong). But how do I reason the validity of the following formulas:

□(a -> b)

□⟡(a ^ b)

?

## migrated from mathoverflow.netFeb 8 '14 at 17:16

This question came from our site for professional mathematicians.

It appears to me that what you have is a Kripke model consisting of four worlds, and you've listed the propositions $a$ and $b$ that happen to be true in each world. You might have meant five worlds, however, since there is a transition into $S_0$, but this doesn't seem to come from any world, so let us ignore that.

Let's assume that by saying that a formula is valid, you mean that it it true at every world. (One might have instead meant that it is true at the initial world; alternatively, people often look at which formulas are valid for a given frame, rather than a specific Kripke model, looking at which formulas are true at every world, regardless of how the propositions are true at the worlds.)

In this case, $\Box a$ is not valid, since $a$ fails at $S_2$, and since $S_0$ accesses $S_2$, we see that $\Box a$ fails at $S_0$.

Similarly, and contrary to what you state, $\Box b$ is not valid, since $b$ fails in $S_2$ and so $\Box b$ fails in $S_0$.

The assertion $\Box (a\implies b)$ is not valid, since the implication $a\implies b$ is false at $S_1$ and so $\Box(a\implies b)$ fails at $S_0$.

The assertion $\Box\Box(a\wedge b)$ is not valid, since $a\wedge b$ fails at $S_1$, and so $\Box(a\wedge b)$ fails at $S_2$, and so $\Box\Box(a \wedge b)$ fails at $S_1$. Basically, the double box construction means that one should check all worlds two steps away, and there is a world two steps from $S_1$ in which $a\wedge b$ fails, and that world is $S_1$ itself.

$\square (a\to b)$ is valind in states where $a\to b$ is valid for all successors. Formula $a\to b$ is valid in $S_2$ and $S_3$, so $\square (a\to b)$ is valid only in $S_1$.

As for $\square\square (a\to b)$, it means that $\square (a\to b)$ has to be valid in all successors. Since this last formula is valid only in $S_1$, there is no state where $\square\square (a\to b)$ is valid.

For the same reason, $\square (a\wedge b)$ is valid in $S_1$ and $S_2$, so $\square\square (a\wedge b)$ is valid only in $S_0$.

• Careful: in temporal logic, $\square p$ means that $p$ is true in all future states (i.e. instead of just direct successors, you deal with the transitive closure). In particular, $\square(a\to b)$ is not valid anywhere in the above system. Also, $\square \square p$ is actually equivalent to $\square p$ in LTL. – Klaus Draeger Feb 10 '14 at 11:55