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

LTL (or PSL) Formula to translateFold

Send

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:

0false

not:

!~

and:

&&&/\

implies:

->-->=>

true:

1true

or:

|||+\/

equivalent:

<-><--><=>

xor:

xor^

LTL

eventually:

F<>

(strong) until:

U

weak until:

W

always:

G[]

(weak) release:

RV

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 {s}|->p {s}(p)

Non-Ov. trigger:

{s}[]=>p {s}|=>p

strong closure:

{s}!

seq:

{s}<>->p

Non-Ov. seq:

{s}<>=>p

Formula SimplificationsFold

basic rewritings
allow larger formulas
syntactic implication
eventuality and universality
language containment
UTF-8 output

Output the (simplified) formula as:
text in Spot's syntax
text in Spin's syntax
text in LBT's syntax
a syntactic tree
property information

Translate the (simplified) formula as:
a deterministic monitor
a nondeterministic monitor

Translate the (simplified) formula as:
a transition-based generalized Büchi automaton
a state-based degeneralized Büchi automaton
a Spin neverclaim

Translate the (simplified) formula as:
a transition-based generalized Büchi automaton
a state-based degeneralized Büchi automaton
then
print an accepting run
draw an accepting run as a lasso-shaped automaton

Translate the (simplified) formula into a Büchi automaton, and then convert it into:
a Testing Automaton (TA)
a Generalized Testing Automaton (GTA)
a Transition-based Generalized Testing Automaton (TGTA)

LTL simplifications
suspension in alternating automaton
suspension in TGBA
on-the-fly simplifications

a-posteriori simplifications
SCC simplifications
more deterministic output
direct simulation on BA

WDBA minimization of intermediate automaton
direct simulation on intermediate automaton
early start of suspended automata
do not compose suspended formulas (for debugging)

Automaton SimplificationsFold

prune unaccepting SCCs
determinize and minimize obligation properties
direct simulation
reverse simulation
iterated simulations