Welcome to the Rabinizer 2 homepage!
Rabinizer 2 is tool generating small deterministic Rabin automata and even smaller deterministic automata with generalized Rabin pairs from LTL formulae.
Automata with generalized Rabin pairs and their use in probabilistic model checking and synthesis is described here. Rabinizer 2 supports LTL formulae using operators X, F, G, and U, where U is not nested within G.
The previous version of Rabinizer only covered F and G operators, see the webpage of Rabinizer. For the definition of the construction and correctness, see here.
The new version of the tool for the whole LTL can be found here.
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.
Update on October 12: a bug in the acceptance condition fixed.
(1) Download Rabinizer 2
The tool can be downloaded as an executable jar file here. Please read also the disclaimer below.
It should run on every machine with a recent Java Runtime Environment / Virtual Machine.
(2) Using Rabinizer
Rabinizer can be invoked as follows (On Windows machines, you might have
to replace java by the path to the java.exe executable, like
java -jar rabinizer.jar ltlfile
input is the path of a file containing a formula from the described fragment of LTL. Examples of valid formulas (temporal operators bind
more strongly than "&" and then "|"):
Atomic variables can be arbitrary strings of alphanumeric characters different from the temporal operators.
Please note that e.g. "Fa" is a single atomic variable, whereas "F a" (a
space separating "F" and "a") denotes an instance of the F-operator.
- 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 ltlfile is read and the corresponding generalized Rabin automaton is computed as well as the respective (degeneralized) Rabin automaton. By default, each constructed item including the acceptance conditions is output into a corresponding file ltlfile.*. The outputs are in the widely used dot format.
There are many viewers and tools available for displaying dot files available; see the graphviz page for more information or a very convenient tool XDot downloadable here.
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".
(3) Output description
In the picture the dot output for the formula G F a & G F b is displayed:
The initial node of the automaton is drawn as an ellipse, the other nodes as
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.
(4) Some experiments
We start with formulae from "Efficient Buchi automata from LTL formulae" on which which ltl2dstar was tested. Here we consider only LTL\GU fragment; for LTL(F,G) see results here. The formulae have been converted to negation normal form. Whenever this transformation affected the size of the ltl2dstar automaton the size is written as a/b where a is the size of the original one and b the size of the automaton for the transformed one.
Further, we illustrate the difference on the following examples where we list sizes of DRA generated by ltl2dstar, DRA generated by Rabinizer 2, and DGRA generated by Rabinizer 2. "T/O" denotes time-out after 15 minutes.
|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))|
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT OWNERS AND CONTRIBUTORS ''AS
IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED
TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
(Last update: April 30, 2012)