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.
Proofs for the tool paper submission to ATVA 2012.
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).
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.
- F a & G (!a | F b)
- G F 1 & G F 0
- ((F G reset) | (G F loc2)) & G test & ! G wait & init
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
Every node is labeled as follows:
For a detailled description of ltl2dstar's output format please visit the ltl2dstar site.
- The first line in a node label displays the formula part and the one-step history of a node (given as propositional formula over the atomic variables),
separated by two double colons.
- The second line contains a tuple of integers, which describes to which automata copy the state belongs. The number of components of the tuple
gives also the number of Rabin pairs, in this case two (see the publication above for details).
- The third line contains the acceptance signature of a node.
The displayed automata has two Rabin pairs (F0, I0), (F1, I1) (F0, I0, F1, I1 are sets of states).
A run (resp. the word read during the run) is accepted by the automaton if there exists a Rabin pair (Fi, Ii) such that no state in Fi is visited
infinitely often and at least one state in Ii is visited infinitely often.
For example, the inital node contains the entries
(I:0) and (F:1). (I:0) means that this state is in I0, and (F:1) that it is also
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.
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)