Input and Output Formats

Owl understand several text-based input and output formats, summarized in the following table:

Format In Out
LTL (+ rLTL) X X
TLSF X
HOA X X
PGSolver X

A more detailed description and links to relevant papers are provided below.

Linear Temporal Logic (LTL)

The grammar for LTL aims to support Spot-style LTL.
For further details on temporal logic, e.g., semantics, see
here.

The following constructs are supported:

Propositional Logic

Precedence Rules

The parser uses the following precedence:

OR < AND < Binary Expressions < Unary Expressions < Literals, Constants, Parentheses

For chained binary expressions (without parentheses), the rightmost binary operator takes precedence.
For example, a -> b U c is parsed as a -> (b U c).

Robust LTL (rLTL)

Owl also supports parsing robust LTL, immediately translating it to LTL, given particular truth values.

Hanoi Omega-Automaton Format (HOA)

Owl supports most of the HOA format, using jhoafparser as back-end.

Caveats:

Temporal Logic Synthesis Format (TLSF)

For use in a synthesis toolchain, Owl supports the basic format of TLSF.

Use syfco to transform other formats into TLSF or LTL.

PGSolver Format

Serialization of parity games into the format used by PGSolver and other parity game solvers like Oink is also supported. See Sec. 3.5 here for a description of the format.