Owl

A tool collection and library for Omega-words, ω-automata and Linear Temporal Logic (LTL).

Quick Start

Download the latest release for your platform from the official website and perform the following steps:

1. Unzip the distribution with: unzip -d <destination> owl-<platform>-<version>.zip
2. Change into the directory containing the executable with: cd <destination>/bin

Usage Examples:

• Translate a LTL formula to a deterministic Rabin automaton:

  $ ./owl ltl2dra -t SE20 -f 'F (a & G b)'
  HOA: v1
  tool: "owl ltl2dra" "<version string>"
  Start: 0
  acc-name: parity min odd 2
  Acceptance: 2 Fin(0) & Inf(1)
  properties: trans-acc no-univ-branch
  properties: deterministic unambiguous
  properties: complete
  AP: 2 "a" "b"
  --BODY--
  State: 0
  [0 & !1 | !0] 0 {0}
  [0 & 1] 1 {1}
  State: 1
  [!1] 0 {0}
  [1] 1 {1}
  --END--
  

• Access the bibliography using:

  $ ./owl bibliography SE20
  [SE20]:
  Salomon Sickert, Javier Esparza:
  "An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata". LICS 2020
  DOI: https://doi.org/10.1145/3373718.3394743
  BibTeX: https://dblp.uni-trier.de/rec/bibtex/conf/lics/SickertE20
  

• Display an overview of all available subcommands:

  $ ./owl --help
  Usage: owl [-hV] COMMAND
  A tool collection and library for ω-words, ω-automata and linear temporal logic.
    -h, --help      Show this help message and exit.
    -V, --version   Print version information and exit.
  Commands:
    ltl2nba           Translate a linear temporal logic (LTL) formula into a
                        non-deterministic Büchi automaton (NBA).
    ltl2ngba          Translate a linear temporal logic (LTL) formula into a
                        non-deterministic generalized Büchi automaton (NGBA).
    ltl2ldba          Translate a linear temporal logic (LTL) formula into a
                        limit-deterministic Büchi automaton (LDBA).
    ltl2ldgba         Translate a linear temporal logic (LTL) formula into a
                        limit-deterministic generalized Büchi automaton (LDGBA).
    ltl2dpa           Translate a linear temporal logic (LTL) formula into a
                        deterministic parity automaton (DPA).
    ltl2dra           Translate a linear temporal logic (LTL) formula into a
                        deterministic Rabin automaton (DRA).
    ltl2dgra          Translate a linear temporal logic (LTL) formula into a
                        deterministic generalized Rabin automaton (DGRA).
    ltl2dela          Translate a linear temporal logic (LTL) formula into a
                        deterministic Emerson-Lei automaton (DELA).
    ltl2delta2        Rewrite a linear temporal logic (LTL) formula into the
                        Δ₂-normal-form using the construction of [SE20].
    ngba2ldba         Convert a non-deterministic (generalised) Büchi automaton
                        to a limit-deterministic Büchi automaton.
    nba2dpa, nbadet   Convert a non-deterministic Büchi automaton to a
                        deterministic parity automaton.
    nbasim            Computes the quotient automaton based on a computed set of
                        similar state pairs.
    aut2parity        Convert any type of automaton into a parity automaton. The
                        branching mode of the automaton is preserved, e.g., if
                        the input automaton is deterministic then the output
                        automaton is also deterministic.
    gfg-minimisation  Compute the minimal, equivalent, transition-based
                        Good-for-Games Co-Büchi automaton for the given
                        deterministic Co-Büchi automaton. The polynomial
                        construction is described in [AK19].
    bibliography      Print the bibliography of all implemented algorithms and
                        constructions. Single references can be looked up by
                        listing them, e.g. 'owl bibliography SE20'. If you want
                        to cite Owl as a whole, it is recommended to use
                        reference [KMS18].
    license           Print the license of Owl and the licenses of all linked
                        (non-system) libraries.
    delag             The functionality of the 'delag' subcommand has been moved
                        to the 'ltl2dela' subcommand. You can use 'owl ltl2dela
                        -t=MS17' to access the original 'delag' construction.
    ltl-utilities     A collection of various linear temporal logic related
                        rewriters.
    rltl2ltl          Convert a robust linear temporal logic (rLTL) formula into
                        a linear temporal logic formula.
    aut-utilities     A collection of various automata related utilities.
  

• Display a specific help message for a subcommand:

  $ ./owl ltl2dpa --help
  Usage: owl ltl2dpa [-hV] [--complete] [--EKRS17-skip-complement]
                     [--skip-acceptance-simplifier] [--skip-formula-simplifier]
                     [--skip-translation-portfolio] [--state-acceptance] [--state-labels]
                     [-o=<automatonFile>] [--SLM21-lookahead=<lookahead>]
                     [-t=<translation>] [-f=<formula> | -i=<formulaFile>]
  Translate a linear temporal logic (LTL) formula into a deterministic parity automaton
  (DPA).
  Usage Examples:
    owl ltl2dpa -f 'F (a & G b)'
    owl ltl2dpa -t SEJK16_EKRS17 -i input-file -o output-file
  To lookup a reference, e.g [SE20], used in this help message please use 'owl
  bibliography'.
        --complete            Output an automaton with a complete transition relation.
        --EKRS17-skip-complement
                              Bypass the parallel computation of a DPA for the negation of
                                the formula. If the parallel computation is enabled, then
                                two DPAs are computed and the smaller one (in terms of
                                number of states) is returned.
    -f, --formula=<formula>   Use the argument of the option as the input formula.
    -h, --help                Show this help message and exit.
    -i, --input-file=<formulaFile>
                              Input file (default: read from stdin). The file is read
                                line-by-line and it is assumed that each line contains a
                                formula. Empty lines are skipped.
    -o, --output-file=<automatonFile>
                              Output file (default: write to stdout).
        --skip-acceptance-simplifier
                              Bypass the automatic simplification of automata acceptance
                                conditions.
        --skip-formula-simplifier
                              Bypass the automatic simplification of formulas.
        --skip-translation-portfolio
                              Bypass the portfolio of constructions from [S19, SE20] that
                                directly translates 'simple' fragments of LTL to automata.
        --SLM21-lookahead=<lookahead>
                              The number of successor states that are explored in order to
                                (1) compute an exact semantic classification of a state, e.
                                g., weak accepting, and (2) in order to compute the
                                'Alternating Cycle Decomposition' [CCF21]. If the number of
                                explored states exceeds this bound, a sound approximations
                                are used as desribed in [SLM21]. If the value is 0, only
                                approximations are used. If the value is negative, then all
                                states are explored and exact semantic information is used.
                                The value is by default -1. If the construction times out,
                                try setting this value to 0 and then increase it again in
                                order to obtain smaller automata. This option only affects
                                the SLM21-translation.
        --state-acceptance    Output an automaton with a state-based acceptance condition
                                instead of one with a transition-based acceptance condition.
        --state-labels        Annotate each state of the automaton with the 'toString()'
                                method.
    -t, --translation=<translation>
                              The default translation is SLM21 and the following
                                translations are available: SEJK16_EKRS17, EKS20_EKRS17,
                                SYMBOLIC_SE20_BKS10, SLM21, SMALLEST_AUTOMATON.
                              SEJK16_EKRS17: Translate the formula to a deterministic
                                parity automaton by combining [SEJK16] with the LDBA-to-DPA
                                translation of [EKRS17]. This translation used to be
                                available through the '--asymmetric' option.
                              EKS20_EKRS17: Translate the formula to a deterministic parity
                                automaton by combining [EKS20] with the LDBA-to-DPA
                                translation of [EKRS17]. This translation used to be
                                available through the '--symmetric' option.
                              SYMBOLIC_SE20_BKS10: Translate the formula to a deterministic
                                parity automaton by combining the LTL-to-DRA translation of
                                [SE20] with DRAxDSA-to-DPA result of [BKS10]. This
                                translation has an _symbolic_ implementation and is
                                provided for testing purposes through this interface. In
                                order to benefit from the symbolic implementation users
                                _must_ use the 'SymbolicAutomaton'-interface.
                              SLM21: Translate the formula to a deterministic parity
                                automaton by combining the LTL-to-DELA translation of
                                [SLM21] with a DELW-to-DPW translation based on
                                Zielonka-trees. Depending on the lookahead either [CCF21]
                                or [SLM21] is used.
                              SMALLEST_AUTOMATON: Run all available DPA-translations with
                                all optimisations turned on in parallel and return the
                                smallest automaton.
    -V, --version             Print version information and exit.
  

Content of the Distribution

Owl is distributed as a platform-specific distributions. Note that the platform-specific distributions contain a platform-independent Java library. A distribution contains the following folders:

• bin - Platform-specific command-line tool.
• doc - Additional documentation.
• jar - Platform-independent Java library, source-code, and documentation.
• lib - Platform-specific C library and headers.

See the format descriptions for a description of accepted inputs. Owl contains a variety of command-line tools originating from Rabinizer 4.0, Delag, and nbadet.

Building a Distribution

If there is no precompiled distribution for your platform available or if you want to use the latest snapshot, follow the build instructions to build your own distribution.

Citing

If you want to cite Owl or one of the implemented constructions, then please refer to the help messages (./owl <subcommand> --help, ./owl bibliography --help) to find the correct reference to cite.