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
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
java -jar rabinizer3.1.jar ‹formula›
‹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.
- F G (a | b U c) & !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 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"
- Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata (ATVA'14)
- From LTL to Deterministic Automata: A Safraless Compositional Approach (CAV'14, invited to JACM)
- Rabinizer 2: Small Deterministic Automata for LTL\GU (ATVA'13)
- Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis (CAV'13)
- Rabinizer: Small Deterministic Automata for LTL(F,G) (ATVA'12)
- Deterministic Automata for the (F,G)-Fragment of LTL (CAV'12)
(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 DRA||Rabinzer 3 DRA||Rabinzer 3 DGRA||Rabinzer 3 DTGRA|
|18 s||2.7 s||1.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.
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)