# 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)

### 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

JLtl2Ba : a Java interface for LTL2BA

Paul Gastin