Welcome to the Rabinizer homepage!

The Rabinizer tool generates small deterministic Rabin automata from LTL formulae. Right now it supports LTL formulae with F and G as temporal operators. The new version of the tool for the whole LTL can be found here.

The tool is based on results of

For the new optimizations implemented in Rabinizer see Rabinizer is written in Java and uses the JavaBDD library.
It is developed at Technische Universität München, Munich, Faculty of Informatics, Chair 7.
For questions contact the authors Jan Kretinsky or Andreas Gaiser (please send bugs, errors etc. to Andreas).

(0) News:

The new version 0.11 fixes some minor problems with the LTL parser.

(1) Test Rabinizer online

For trying out Rabinizer online follow this link . If there are any problems please use the downloadable jar file.

(2) Download Rabinizer

You can download the tool as an executable jar file here (v0.11) . Please read also the disclaimer below.
It should run on every machine with a recent Java Runtime Environment / Virtual Machine. We tested it on Linux, Windows Vista and Mac OS X.

(3) 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 (-dot | -ltl2dstar) input output [-verbose]

input is the path of a file containing a formula from the (F,G)-fragment of LTL. Examples of valid formulas (F, G binds more strongly than "&" and "|"): Atomic variables can be arbitrary strings of alphanumeric characters (except "F" and "G"). 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.
output is the name of the desired output file. If -dot is specified, Rabinizer will output a file output.dot which displays the resulting automaton 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. If -ltl2dstar is specified, Rabinizer will output the automaton in the format of the determinization tool ltl2dstar. If the option -verbose is specified, Rabinizer also outputs the generalized Rabin acceptance condition in a file output.acc, and the initial automaton (created before the degeneralization of the Rabin conditions) in output_initial.dot.

(4) Output description

In the picture the dot output for the formula G (a | F b) is displayed:

The initial node of the automaton is drawn as a box with additional edges in the corners, the other nodes as ordinary boxes. Every node is labeled as follows: For a detailled description of ltl2dstar's output format please visit the ltl2dstar site.

(5) Notes

Please ignore messages like

Could not load BDD package buddy: Can't load library : ***buddy.***

while running Rabinizer. The tool uses the Java implementation of JavaBDD and thus does not need the native libraries of the Buddy BDD package.

(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.
(Saturday, 28th of April, 2012)