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 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.
Older releases can be found in the archive.
You can try the different subcommands here.
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.
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:
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