A tool collection and library for Omega-words, ω-automata and Linear Temporal Logic (LTL).
Download the latest release for your platform from the official website and perform the following steps:
unzip -d <destination> owl-<platform>-<version>.zip
cd <destination>/bin
Usage Examples:
$ ./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--
$ ./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
$ ./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.
$ ./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.
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.
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.
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.