LTL – linear time temporal logic formulae for specifying correctness requirements.

SYNTAX

Grammar:
ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl

Operands (opd):
true, false, and user-defined names starting with a lower-case letter.

Unary Operators (unop):
[] or G (the temporal operator always)
<> or F (the temporal operator eventually)
! (the boolean operator for negation)
X (next)

Binary Operators (binop):
U (the temporal operator strong until)
V or R (release: the dual of U): (p V q) means !(!p U !q))
&& (the boolean operator for logical and)
|| (the boolean operator for logical or)
/ (alternative form of &&)
/ (alternative form of ||)
-> (the boolean operator for logical implication)
<-> (the boolean operator for logical equivalence)

DESCRIPTION
Our tool will translate LTL formulae into never claims automatically. So you do not need to write the negation for the property to be checked. The never claim that is generated encodes the Buchi acceptance conditions from the LTL formula. Formally, any omega-run that satisfies the LTL formula is guaranteed to correspond to an accepting run of the never claim.

All binary operators are left-associative. Parentheses can be used to override this default. Note that implication and equivalence are not temporal but logical operators.

EXAMPLES
[] p
!( <> !q )
p U q
p U ([] (q U r))