# Given LTL formulas $m$ and $p$, is there a tool that can check whether $m \models p$ does hold?

To the best of my understanding, $$m \models p$$ asks whether the LTL formula $$p$$ satisfies the LTL formula $$m$$. In other words, $$m \to p$$ is a tautology. Here are some examples of where $$m \models p$$ holds:

Xp |= Fp

q  |= p U q

Gq |= Fq


Of course, trying to visualise all this in you head and trying to work out if $$m \models p$$ holds can get very time consuming, especially if $$m$$ and $$p$$ are very long. So, I was wondering there is some tool/software/platform that can compute $$m \models p$$.

Yes, you can use an LTL-to-Büchi-automaton translator for this.

Let's assume that you want to check if $$\psi \rightarrow \psi'$$ is a valid LTL formula, i.e., every word satisfying the LTL property $$\psi$$ also satisfies the LTL property $$\psi'$$. This case is equivalent to finding out if $$\psi \wedge \neg \psi'$$ is satisfiable. Your $$\psi \models \psi'$$ notation is another way of writing this, but I would avoid it since the $$\models$$ relation is often defined differently in current research papers on the topic.

If we translate $$\psi \wedge \neg \psi'$$ to a Büchi automaton, we can easily check if its language is empty. In fact, optimizing LTL-to-Büchi translators remove states with an empty language, and hence you only need to check if the resulting automaton has no accepting state.

On example LTL-to-Büchi translator is ltl3ba. For instance, if you want to check if $$\mathsf{F G }\,a$$ implies $$\mathsf{G F}\,a$$, you can do that as follows:

./ltl3ba -f "(F G a) && !(G F a)"


Here, "-f" stands for "translate this formula that is given as a parameter".

The result is given in SPIN never claim form:

never {    /* (F G a) && !(G F a) */
T0_init:
false;
}


There is no state ending with "_accept" in the name, which means in the SPIN never claim notation that there is no accepting state. So $$(\mathsf{F G }\,a) \wedge \neg (\mathsf{G F}\,a)$$ is not satisfiable.

There is also at least one LTL-to-Büchi translator with a web interface, namely the one from the SPOT framework.