LTL 2 BA : fast translation from LTL formulae to Büchi automata

Software written by Denis Oddoux (v1.0) and modified by Paul Gastin (v1.2 & v1.3)

Warning: Due to some security settings on the web server (preventing code injections) some formulae containing negations '!' induce an error (403).
In such cases, use 'NOT' (upper case) instead of '!' for negations.

LTL formula: (Memory limit : 1 Gb, Time limit: 2 hours)

Use Spin syntax
Use Spin 4.3.0

Display an image of the generalised Büchi automaton
Display an image of the Büchi automaton
echo a never claim for Spin

Use verbose mode
Display time and size statistics

Enable on-the-fly automata simplification
Enable a posteriori automata simplification
Enable strongly connected components simplification
Consider second set in fj->fj (internal use)

How can I use this form ?

Enter in the form an LTL formula and check all the boxes you want.

An LTL formula may contain propositional symbols, boolean operators, temporal operators, and parentheses.
Use spaces between any symbols.

Propositonal Symbols: 

        true, false
	any lowercase string
Boolean operators (no priority, use parentheses): 
        !   (negation)
        ->  (implication)
        <-> (equivalence)
        &&  (and)
        ||  (or)
Temporal operators (no priority, use parentheses): 
        G   (always) (Spin syntax : [])
        F   (eventually) (Spin syntax : <>)
        U   (until)
        R   (realease) (Spin syntax : V)
        X   (next)
Our program can draw automatically the resulting automaton, and can also print a never claim that can be given to the Spin model checker to verify properties on a system.

Automatas are drawn by 'dot', a program devellopped in the Graphviz package.

The LTL2BA software was written by Denis Oddoux and modified by Paul Gastin.
It is based on the paper Fast LTL to Büchi Automata Translation presented at CAV '01.
See also Denis Oddoux's thesis (in french).
Download LTL2BA
JLtl2Ba : a Java interface for LTL2BA
Paul Gastin