Owl is a command-line tool and a library of algorithms designed to support researchers in formal methods and developers to work with ω-words, ω-automata, and linear temporal logic (LTL). It implements several state-of-the-art constructions used for synthesis of reactive systems and model-checking probabilistic systems. Owl provides the following notable features:
- Translation of LTL and robust LTL to non-deterministic, limit-deterministic, and deterministic ω-automata (including symbolic ω-automata)
- Rewriting of LTL into the Δ₂-fragment of LTL
- Conversion of Emerson-Lei automata into parity automata
- Determinisation and limit-determinisation of non-deterministic (generalised) Büchi automata
- Minimisation of Good-for-Games coBüchi automata
- LTL simplifier
- Language-emptiness checker
Detailed bibliographic information for each implemented construction is available through owl <subcommand> --help and owl bibliography.
Owl supports LTL, robust LTL, and ω-automata with arbitrary acceptance conditions in the HOA format using jhoafparser. While all implemented algorithms are designed to work with transition-based acceptance conditions, there is an option to select state-based acceptance conditions. A description of the supported formats is contained in FORMATS.md.
Downloads
Platform-specific distributions are available for Linux (amd64) and macOS (amd64) and contain Owl as a native command-line tool, as a Java 11 library, and as a native C library. Note that the Java 11 library can be used on all platforms that are supported by a JDK for Java 11. Native builds for other platforms, e.g. Windows (amd64) and Linux (aarch64), are currently not provided. Please contact the maintainer of Owl if you need access to such builds. Using GraalVM the Java 11 library can be also used from JavaScript (Node.js), R, Ruby, and Python.
The latest release is 21.0 which was published on the 30.10.2021 (changelog). Here are the convenience links for this release:
Older releases can be found in the archive.
Online Demo
You can try the different subcommands here.
Development and License
Development of Owl happens on GitHub. Owl is licensed under GPLv3. If this licence is incompatible with your project, please contact the maintainers of Owl to find a solution.
Contact
Release announcements are published on GitHub. If you encounter a problem, need support, or have a question about Owl please open an issue on GitHub.
Related Projects
Owl was created from the previously existing tool ltl2ldba. Further, it bundles the translation from the following existing tools and provides improvements:
The following projects are using Owl:
- Strix is a tool for synthesising reactive controllers from LTL specifications. Owl is used to parse LTL formulas and to translate them to deterministic automata.
- MoChiBA uses the LDBAs generated by Owl for probabilistic model checking.
- OmegaThreads: OmegaThreads is a tool for parallel automated controller synthesis for dynamical systems to satisfy ω-regular specifications given as LTL formulas.
- PRISM: A Probabilistic Symbolic Model Checker.
Citing
If you want to cite Owl in an academic publication, please use the following reference:
- Jan Křetínský, Tobias Meggendorfer, Salomon Sickert
Owl: A Library for ω-Words, Automata, and LTL
ATVA (2018): bibtex / view / preprint
If you want to cite a particular translation or construction, then please refer to the citations found in the help messages of the subcommand (owl <subcommand> --help) and to the included database of citations, which is available through the command owl bibliography.