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