Rabinizer 2 is written in Java and is developed at Technical University Munich, Faculty of Informatics, Chair 7.
For questions contact the authors
Jan Kretinsky or Ruslan Ledesma Garza.
For running Rabinizer 2 without printing the automata to files (which takes some time) one can use the flag "-nodot". For more information use "-h".
ltl2dstar | Rabinzer 2 | Formula |
3 | 3 | p U q |
4 | 4 | p U (q U r) |
3 | 4 | F p U G q |
5 | 5 | (G p) U q |
4 | 3 | (p | q) U p | G q |
4 | 4 | (X p) U (X q) | X (!q U (!p & !q) | G !q) |
4 | 3 | (X p) U q | X ((!p | !q)U !p | G(!p | !q) ) |
19/26 | 8 | G(!p | F q) & ((X p)U q | X((!p | !q)U !p | G(!p | !q))) |
4/20 | 10 | G(!p | F q) & ((X p)U (X q) | X((!q)U (!p & !q) | G(!q))) |
4 | 5 | F(p & X(!r U (!q & !r) | G!r)) |
5 | 14 | G(q | X G p) & G(r | X G !p) |
3 | 3 | G(q | (X p & X !p)) |
3 | 3 | (p U p) | (q U p) |
ltl2dstar DRA | Rabinzer 2 DRA | Rabinzer 2 DGRA | Formula |
353 | 73 | 73 | ((G F (a & X X b) | F G b) & F G (c | (X a & X X b))) |
2127 | 169 | 85 | G F (X X X a & X X X X b) & G F (b | X c) & G F (c & X X a) |
18176 | 80 | 40 | (G F a | F G b) & (G F c | F G (d | X e)) |
16013 | 45 | 45 | (G F (a & X b) | F G (b | X !a)) & (G F (b | X c) | F G (!c | X a)) |
78150 | 101 | 53 | (G F (a & X b) | F G (b | X !a)) & (G F (b & X c) | F G (!c | X a)) |
T/O | 142 | 142 | (G F (a & X X c) | F G b) & (G F c | F G (d | X a & X X b)) |
T/O | 210 | 60 | a U b & (G F a | F G b) & (G F c | F G d) | a U c & (G F a | F G d) & (G F c | F G b) |
24252 | 361 | 181 | G F(a & X X b) U (G F(b & X c) & G F(c & X X a)) |
T/O | 181 | 181 | G F(a & X X b) U (G F(b & X c) U G F(c & X X a)) |
T/O | 181 | 181 | (G F(a & X X b) U G F(b & X c)) U G F(c & X X a) |
T/O | 2061 | 103 | (G F (a & X b) | F G (b | X !a)) & (G F (b & X c) | F G (!c | X a)) & (G F (b & X X a) | F G (!c | X !b)) |
T/O | T/O | 107 | (G F (a & X b) | F G (b | X !a)) & (G F (b & X c) | F G (!c | X a)) & (G F (b & X X a) | F G (!c | X !b)) & (G F (b & X X !c) | F G (!a | X !b)) |