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:
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.