Rabinizer 4 online demo

Developed by Jan Křetínský, Tobias Meggendorfer, and Salomon Sickert. See the Rabinizer 4 webpage for further information.

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

Format:

DGRA (Rabinizer construction)
DRA (Rabinizer + Degeneralization)
DPA (Rabinizer + Degeneralization + IAR construction)
DPA (LDBA construction)
DPA (LDBA construction, Guessing F)
LDBA
LDBA (Guessing F)

Options:

Show state annotations (Warning: Large pictures)
Use a simple statespace construction
State based acceptance
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.