Owl (20.06) Online Demo

Input:

Some formulas to try out (simply copy-paste them in the above field):

(G F a) -> (G F b)
F G a | G F b
a & X G (a U XXb) | !a & X G (a U XXc)
G (!a & (b U (!c U (!d | e))))
G ((a1 & F b1) | (a2 & F b2))
(X a) W (b M c XOR G a) <-> a R c
F a & F b & F G c

Translation to:

NBA
NGBA
LDBA (symmetric construction)
LDGBA (symmetric construction)
LDBA (asymmetric construction)
LDGBA (asymmetric construction)
DRA (symmetric construction)
DGRA (symmetric construction)
DRA (asymmetric construction)
DGRA (asymmetric construction)
DPA (intermediate symmetric LDBA construction)
DPA (intermediate asymmetric LDBA construction)
DELA (deterministic Emerson-Lei)
N*A (portfolio translation to nondeterministic automata)
D*A (portfolio translation to deterministic automata)
∆2 Normalform

Automata Translation Options:

Show state annotations (Warning: Large pictures)
Highlight SCCs (green: contains acc cycle, red: contains no acc cycle, black: trivial, gray: useless)

We use Spot's autfilt to convert the result into the dot format and render it to SVG using the equally named tool.