Rabinizer 2

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.

(0) News

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 C:\Programs\Java\bin\java.exe):

java -jar rabinizer.jar ltlfile

where 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 "|"):

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

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

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

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)

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.

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

(5) Disclaimer

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)