Logo.

Owl

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

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:

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.

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:

Citing

If you want to cite Owl in an academic publication, please use the following reference:

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.