Owl understands several text-based input and output formats, summarized in the following table:
| Format | In | Out |
|---|---|---|
| LTL (+ rLTL) | X | X |
| HOA | X | X |
| PGSolver | X |
A more detailed description and links to relevant papers are provided below.
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:
tt, true, 1ff, false, 0[a-zA-Z_][a-zA-Z_0-9]* or quoted "[^"]+"!, NOT->, =>, IMP<->, <=>, BIIMP^, XOR&&, &, AND||, |, OR(, )FGXUWRMThe 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).
Owl also supports parsing robust LTL, immediately translating it to LTL, given particular truth values.
Owl supports most of the HOA format, using jhoafparser as back-end.
Caveats:
Use syfco to transform TLSF to LTL. For example: syfco FILE -f ltlxba -m fully.
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.