Logo.

Owl

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

Owl is a Java 10+ tool collection and library for ω-words, ω-automata and linear temporal logic. It provides a wide range of algorithms for automata and LTL. It has the following notable features:

Further, it includes several translations from LTL to ω-automata and bundles the following existing tools:

Download and Installation

The latest version is 18.06, was released on the 29.6.2018 and can be downloaded here:

Detailed build instructions can be found in BUILDING.md and usage instructions in USAGE.md. A description of the supported formats is contained in FORMATS.md. Older release can be found in the archive.

The API documentation of the latest stable release is available online as Javadoc.

Online Demo

You can try the tools here.

Contact

Release announcements are published on the i7-project-announcements mailing list.

For general feedback, comments and questions contact Jan, Salomon and Tobias. If you have specific questions related to the code please contact Salomon and Tobias.

Apart from the bundled projects Delag and Rabinizer 4.0 there are the following projects we are aware of using Owl:

Citing

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

To refer to a particular translation, you may consider some of the references below:

History

Owl was created from the existing tool ltl2ldba and was based in parts on code originating from Rabinizer 3.1.