How to transform LTL into Automato in Promela - SP

Question

How can I transform LTL into Automata in PROMELA? I know that with the command SPIN -f "ltl x" it is possible transform the LTL into a never claim, but I want the automata of the LTL and not the negation one. It is correct If I negate the LTL before to generate the never claim. Can anyone help me?

Answer 1

Spin generates the Promela code equivalent to the Buchi Automaton which matches the LTL formula, and envelops it into a never block.

From the docs:

NAME never - declaration of a temporal claim.

SYNTAX never { sequence }

DESCRIPTION A never claim can be used to define system behavior that, for whatever reason, is of special interest. It is most commonly used to specify behavior that should never happen. The claim is defined as a series of propositions, or boolean expressions, on the system state that must become true in the sequence specified for the behavior of interest to be matched.

Therefore, if you want to have a look at the code that matches a given LTL formula, you can simply type:

~$ spin -f "LTL_FORMULA"

e.g.:

~$ spin -f "[] (q1 -> ! q0)" 
never  {    /* [] (q1 -> ! q0) */
accept_init:
T0_init:
    do
    :: (((! ((q0))) || (! ((q1))))) -> goto T0_init
    od;
}

An alternative way for obtaining the same code, plus a graphic representation of the Buchi Automaton, is to follow this link.

---

Looking at both your comments and this other question of yours, it appears that you want to check whether two LTL formulas p and g contradict each other, that is whether it is definitively the case that a model satisfying p would necessarily violate g and vice-versa.

This could be theoretically done using spin. However, this tool does not simplify the code of the Buchi Automaton and therefore it is difficult to deal with its output.

I would reccomend you to download LTL2BA (at the following link) instead. To set it up, you just need to unpack the tar.gz file and type make in the console.

Let's see a usage example:

~$ ./ltl2ba -f "([] q0) && (<> ! q0)"
never {    /* ([] q0) && (<> ! q0) */
T0_init:
    false;
}

Since [] q0 and <> ! q0 contradict each other, the returned Buchi automaton is empty [n.b.: by empty i mean that it has no accepting execution]. In this context, the code never { false; } is the canonical form of an empty Buchi Automaton without any accepting execution.

---

Disclaimer: comparing the output with never { false } to decide whether the Buchi Automaton is empty or not, might lead to spurious results if the simplification steps are unable to transform all empty automatons in the canonical form.