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

Modal 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)

Use syfco to transform TLSF to LTL. For example: syfco FILE -f ltlxba -m fully.

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.