LTL Input Grammar

All tools based on Owl understand the same LTL input language.
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).