Spot Logo

Translator of LTL to Transition-based Generalized Büchi Automata

LTL (or PSL) Formula to translateFold


Use alphanumeric identifiers or double-quoted strings for atomic propositions, and parentheses for grouping.
Identifiers cannot start with the letter of a prefix operator (F, G, or X): for instance GFa means G(F(a)). Use "GFa" if you really want to refer to GFa as a proposition.
Conversely, infix letter operators are not assumed to be operators if they are part of an identifier: aUb is an atomic proposition, unlike a U b and (a)U(b).

Constants Unary operators Binary operators (infix)
Boolean false:0 false not:! ~ and:& && /\ implies:-> --> =>
true:1 true or:| || + \/ equivalent:<-> <--> <=>
xor:xor ^
LTL eventually:F <> (strong) until:U weak until:W
always:G [] (weak) release:R V strong release:M
next:X ()
SERE ε:[*0] Kleene star:[*] [+] [*i..j] concatenation:; fusion::
goto:[->i..j] intersection:&& /\ NLM and:&
nonconsec. rep.:[=i..j] union:| || + \/
iterated fusion:[:*] [:+] [:*i..j]
PSL weak closure:{s} triggers:{s}[]->p
Non-Ov. trigger:{s}[]=>p
strong closure:{s}! seq:{s}<>->p Non-Ov. seq:{s}<>=>p

Formula SimplificationsFold

Output the (simplified) formula as:

Translate the (simplified) formula as:

Translate the (simplified) formula as:

Translate the (simplified) formula as:


Translate the (simplified) formula into a Büchi automaton, and then convert it into:

Use LTL3BA to build: or

Automaton SimplificationsFold

Emptiness-check AlgorithmFold

Search accepting run using algorithm: with these options:

Testing Automaton OptionsFold