Rabinizer 4

From LTL to Your Favourite Deterministic Automaton

Rabinizer 4 is a tool set for generating small deterministic ω-automata from LTL (linear temporal logic) formulas

It translates LTL to various types of automata, e.g. (generalized) Rabin, parity, or limit-deterministic Büchi.
It is linked to the probabilistic model checker PRISM and a parity-game solver PGSolver and thus can be used for probabilistic model checking and for synthesis.
It is free and open source, distributed under the GNU General Public License (GPL), version 3, and can be downloaded here.
For more detail, see the Rabinizer 4 tool paper.
It is built using Owl.
Should you have any questions or suggestions, please contact {jan.kretinsky, tobias.meggendorfer, sickert} AT in.tum.de.

Online Demo & Quick Guide

Try the online demo for Rabinzer 4 and other Owl tools here. The tool can also be downloaded here or as a virtual machine here. Its bin folder contains several scripts. For example, the command

bin/ltl2dpa "GFa & GFb"

translates the LTL formula GFa ∧ GFb into a deterministic parity automaton. The command

bin/ltl2dgra --annotations "GFa & GF(b & X!b)"

translates the LTL formula GFa ∧ GF(b ∧ X¬b) into a deterministic generalized Rabin automaton, labelling its states with their logical semantics. This command replaces previous versions of Rabinizer.

Functionality

Rabinizer features several translations, which can be run by the following scripts:

ltl2dra -- translates LTL to deterministic Rabin automata
ltl2dgra -- translates LTL to deterministic generalized Rabin automata
ltl2ldba -- translates LTL to limit-deterministic Büchi automata
ltl2ldgba -- translates LTL to limit-deterministic generalized Büchi automata
ltl2dpa -- translates LTL to deterministic parity automata
fltl2dgmra -- translates the frequency extension of LTL to deterministic generalized mean-payoff Rabin automata

The constructions are tested using multiple tools from the Spot library. All tools support a --help switch, which briefly explains the available options.

Usage

The scripts, e.g., ltl2dgra, are invoked as follows:

bin/ltl2dgra ‹formula›

where ‹formula› is an LTL formula using operators X, F, G, W, R, M, U, !, &, ∣, atomic propositions (alphanumeric string starting with a lowercase letter), parentheses, true, false, and some more. A precise definition of the input grammar can be found in FORMATS.md. Examples of valid formulas are:

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
(G F a XOR G b) <-> ((a R c) W (G F d))

The above call outputs a transition-based generalized Rabin automaton in the HOA format. This automaton can be converted to the popular dot format by piping it to autfilt --dot. Dot files can be viewed by dot-viewers, such as XDot, or rendered to PNG / SVG by further piping to the dot executable (dot -Tpng / dot -Tsvg). To include semantic labelling, add --annotations as the first parameter. For example, to obtain an image of a DGRA recognizing the formula a ∨ G b, execute the following command (on Linux):

bin/ltl2dgra --annotations "a | G b" | autfilt --dot | dot -Tpng > automaton.png

The input set can also be read from and written to files as follows:

bin/ltl2dgra --annotations -I "input.ltl" -O "output.hoa"

Publications

For an overview of relevant papers please have a look at the citing page.

Previous Versions

Previous versions of the tool can be found at the following locations:

Rabinizer 3 can be found here.
Rabinizer 2 (only supporting LTL\GU) can be found here.
Rabinizer 1 (only supporting LTL with F- and G-operators) can be found here.

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: June 28, 2018)