21.0

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.

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.

Here are the convenience links for this release:

• Owl 21.0 for Linux (amd64)
• Owl 21.0 for macOS (amd64)
• Javadoc for Owl 21.0