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: (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)


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