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


1 Answer 1


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) */

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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