Welcome to the Rabinizer 3 homepage!

Rabinizer 3 is a tool generating small deterministic Rabin automata and even smaller deterministic generalized Rabin automata from LTL formulae. It is free and open source. You can download both the tool and its source code for free below. Distribution is under the GNU General Public License (GPL), version 2. The tool has been tested using ltlcross. The algorithm implemented has been proven correct in Isabelle. For questions please contact Jan Kretinsky.

(0) News

Jul 21 2015: Version 3.1 features symbolic exploration of automata transitions and thus speeds up the construction for formulae with many atomic propositions significantly.
Feb 1 2015: Hanoi omega-automata format (HOAF) supported in Rabinizer 3

(1) Download Rabinizer 3

The current version of Rabinizer 3.1 (incl. sources) is available here.

(2) Using Rabinizer

Rabinizer 3.1 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 rabinizer3.1.jar ‹formula›

where ‹formula› is an LTL formula using operators X, F, G, !, U, &, ∣ (binding in this order), atomic propositions (alphanumeric string starting with a letter) parentheses (, ), and true, false. Examples of valid formulas: Please note that e.g. "Fa" is a single atomic variable, whereas "F a" (a space separating "F" and "a") denotes an application of the F operator.
Upon the call above, the formula is read and the corresponding transition-based generalized Rabin automaton is computed. The outputs are in the widely used dot format. The initial state is drawn as an ellipse, other states as boxes; the acceptance condition uses brackets as set delimiters. There are many viewers and tools for displaying dot files available; see the graphviz page for more information or a very convenient tool XDot downloadable here.

Rabinizer can also produce other types of automata and in other formats. For full usage, please run "java -jar rabinizer3.1.jar -h"


(3) Papers


(4) Some experiments

Results on benchmark used in "From LTL to deterministic automata: A Safraless compositional approach" can be found here.

A PRISM example with Pnueli-Zuck protocol with 3 processes has 2368 states; the property considered is Pmax=? [F G (p1 != 0) | (G F (p1 = 10)) & (G F (p2 = 10)) & (G F (p3 = 10))]. The sizes of the automaton, number of pairs, product sizes and analysis times are the following:
ltl2dstar DRARabinzer 3 DRARabinzer 3 DGRARabinzer 3 DTGRA
102917 1
5222
32224604423682368
18 s2.7 s1.2 s


(5) Older versions and connecting to PRISM

The previous version Rabinizer 3 can be downloaded as an executable jar file here or as source code here. The PRISM extension used for the paper ``Rabinizer 3'' can be downloaded as source code here. For the official release of PRISM, which supports translators with output in HOA format (incl. Rabinizer), see here. It should run on every machine with a recent Java Runtime Environment / Virtual Machine.

The older version of the tool for the fragment of LTL with F and G operaors can be found here and for the fragment LTL\GU here.


(6) 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: Feb 12, 2016)