Rabinizer 4

From LTL to Your Favourite Deterministic Automaton

Rabinizer 4 is a tool set for generating small deterministic ω-automata from LTL 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 and Basic Usage

Rabinizer features various transformations presented in the following table. They are named "‹x›2‹y›", where ‹x› denotes the input type (e.g., ltl) and ‹y› the output type (e.g., dgra).

x2y dgra dra ldba dpa dgmra
ltl x x x x
fltl x
nba x x
dgra x
dra x

where ltl, fltl, nba, dgra, dra, ldba, dpa, dgmra stand for linear temporal logic, its frequency extension, non-deterministic Büchi, deterministic generalized Rabin, deterministic Rabin, limit-deterministic Büchi, deterministic parity, deterministic generalized mean-payoff Rabin automata, respectively. For more detail, see the Rabinizer 4 tool paper. The constructions are tested using multiple tools from the Spot library. All tools support a --help switch, which briefly explains the available options.

LTL to automata translations

The ltl2‹y› constructions, 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 pipeing 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"

Automata to automata translations

The automaton based constructions, e.g., nba2dpa, expect input in the HOA format. Usually, these are either piped from other tools

ltl2tgba -H ‹formula› | bin/nba2dpa

or read from a file

bin/nba2dpa -I "input.hoa"

Papers (Selection)

Owl

Rabinizer 4 is backed by a multi-purpose omega-automaton library and LTL library, named Owl. Since many LTL to automaton translations (or translations involving automata, in general) have a lot of basic requirements in common, we developed a flexible library providing commonly used building blocks through efficient implementations. Its intended use is rapid prototyping and developement of potential algorithms without the need of dealing with "infrastructure", e.g. tinkering with external BDD libraries written in C, implementing parsing and representation of automata, setting up test-enviroments, etc. Everything needed to start developing new procedures is an up-to-date JDK and a copy of the sources.

Already in a stable state, Owl is constantly being extended and improved. We are more than happy about suggestions, feedback, potential bug-reports, use cases or even collaboration, all of which can be done through our GitLab.

Extended command line syntax

Owl comes with a flexible command line interface intended to aid rapid development and prototyping of various constructions. To give full control over the translation process to the user, it offers a verbose, modular way of specifying a particular toolchain. This is achieved by the means of multiple building blocks, namely coordinators, input parsers, transformers, and output writers, all of which are completely pluggable and extendable.

Firstly, coordinators are responsible for setting up input and output behaviour. Usually, users will be content with reading from standard input or a file, which is handled by our stream coordinator. Other possible coordinators will be mentioned later.

The other three blocks are, as their names suggest, responsible for parsing input, applying operations to objects, and serializing the results, respectively. For example, we chain an LTL parser to the ltl2dpa construction, followed by parity minimization and hoa output by

owl --- stream --- ltl --- ltl2dpa --- minimize-aut --- hoa

To read from some file "input.ltl" and write to "output.hoa", we simply have to change the parameters of the coordinator to

owl --- stream -I "input.ltl" -O "output.hoa" --- ltl --- ltl2dpa --- minimize-aut --- hoa

Now, suppose we want to first pre-process the LTL formula. To this end, we simply add another transformer to the pipeline as follows.

owl --- stream --- ltl --- rewrite --mode modal-iter --- ltl2dpa --- minimize-aut --- hoa

For research purposes, we might be interested in what exactly happens during the intermediate steps, for example how the rewritten formula looks like, or how large the automaton is prior to the minimization. These values could be obtained by running different configurations, but this is rather cumbersome. Instead, we offer the possibility of seamlessly collecting meta-data during the execution process. For example, to obtain the above numbers in one execution, we write

owl --- stream --- ltl --- rewrite --mode modal-iter --- string --- ltl2dpa --- aut-stat --format "States: %S SCCs: %C Acc: %A" --- minimize-aut --- hoa

Owl will now output the requested information together with the corresponding input to stderr (by default).

Often, a researcher might not only be interested in how the existing operations performs, but rather how a new implementation behaves. By simply delegating to an external translator, existing implementations can easily be integrated in such a pipeline. For example, to delegate translation to the old Rabinizer 3.1, we could simply write

owl --- stream --- ltl --- rewrite --mode modal-iter --- unabbreviate -r -w -m --- ltl2aut-ext --tool "java -jar rabinizer3.1.jar -format=hoa -silent -out=std %f" --- minimize-aut --- hoa

The real strength of the implementation comes from its flexibility. The command-line parser is completely pluggable and written without explicitly referencing any of our implementations. To add a new algorithm to the pipeline, one simply has to provide a name (as, e.g., ltl2nba), an optional set of command line options and a way of obtaining the configured translator from the parsed options. For example, supposing that this new ltl2nba command has some --fast flag, the whole description necessary is as follows:

public class LTL2NBASettings implements TransformerSettings {
  public Factory createTransformerFactory(CommandLine settings) {
    boolean fast = settings.hasOption("fast");
    return environment -> (input, context) -> LTL2NBA.apply((LabelledFormula) input, fast, environment);
  }
  public String getKey() { return "ltl2nba"; }
  public Options getOptions() {
    return new Options().addOption("f", "fast", false, "Turn of fast mode");
  }
}

After registering these settings, the tool can now be used exactly as ltl2dpa before. Parsers, serializers or even coordinators can be registered with the same kind of specification. Similarly, dedicated command line tools like our presented ltl2dgra or nba2dpa can easily be created by delegating to this generic framework. For example, ltl2ldba is created by

public static void main(String... args) {
  SingleModuleParser.run(args, ImmutableSingleModuleConfiguration.builder()
    .inputParser(new LtlInput())
    .addPreProcessors(new RewriterTransformer(RewriterEnum.MODAL_ITERATIVE))
    .transformer(new LTL2LDBAModule())
    .outputWriter(new HoaWriter())
    .build());
}

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: Nov 02, 2017)