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.

It should run on every machine with a recent Java Runtime Environment / Virtual Machine.

where

- G (a | X b) & !a U (b U X c)
- G F a & G F b
- ((F G reset) | (G F loc2)) & G test & ! G wait & init

Upon the call above, the formula from file

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".

The initial node of the automaton is drawn as an ellipse, the other nodes as ordinary boxes. Every node is labeled as follows:

- The first part (before ::) displays the formula part of the state space.
- The second part (after ::) displays the current states of the "segment" automata B(xi), whose dot representation is also output.
- Moreover, for Rabin automata the additional second line contains a tuple of integers, which describes to which degeneralization copy the state belongs:
- The generalized Rabin acceptance conditions is a set of generalized Rabin pairs (as described here) where the first component is the set to be visited only finitely often, while the second component is a set of sets each of which is to be visited infinitely often. For the Rabin condition, the second component is always a singleton.

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)) |