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.1)

LTL formula:

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.

Propositonal Symbols: 

        true, false
	any lowercase string
Boolean operators: 
        !   (negation)
        ->  (implication)
	<-> (equivalence)
        &&  (and)
        ||  (or)
Temporal operators: 
        G   (always) (Spin syntax : [])
        F   (eventually) (Spin syntax : <>)
        U   (until)
        R   (realease) (Spin syntax : V)
        X   (next)
Use spaces between any symbols.

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
LTL2BAIF : a Java interface for LTL2BA
Paul Gastin