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.
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
, 1
ff
, false
, 0
[a-zA-Z_][a-zA-Z_0-9]*
or quoted "[^"]+"
!
, NOT
->
, =>
, IMP
<->
, <=>
, BIIMP
^
, XOR
&&
, &
, AND
||
, |
, OR
(
, )
F
G
X
U
W
R
M
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)
.
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:
For use in a synthesis toolchain, Owl
supports the basic format of TLSF.
Use syfco to transform other formats into TLSF or LTL.
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.