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

Owl is a Java 11 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:

For reference, an annotated prototype implementation of Safra’s construction can be here. Further, an overview over the code metrics, demonstrating potential savings can be found here.

Download and Installation

The latest version is 19.06.03, was released on the 22.7.2019 (changelog) 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.


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:


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:


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