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

Online Demo & Quick Guide

Try the tool online 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: 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 more formal definition by an ANTLR grammar can be found in the source code (src/main/antlr). Examples of valid formulas:

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"

Papers (Selection)

Older Versions

The previous version Rabinizer 3 can be found here. The older version of the tool for the fragment of LTL with F and G operators can be found here and for the fragment LTL\GU 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: Feb 15, 2018)