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.
