NAME
LTL - linear-time temporal logic formulae, for specifying correctness requirements.

SYNTAX

Grammar:
	ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl
Unary Operators (unop):
	[]   (the temporal operator always),
	<>   (the temporal operator eventually),
	!   (the boolean operator for negation)
Binary Operators (binop):
	U   (the temporal operator strong until)
	V   (the dual of U): (p V q) == !(!p U !q)
	&&   (the boolean operator for logical and)
	||   (the boolean operator for logical or)
	->   (the boolean operator for logical implication)
	<->   (the boolean operator for logical equivalence)
Operands (opd):
	Predefined: true, false
	User-defined: names starting with a lowercase letter.

DESCRIPTION
Promela itself does not include syntax for linear temporal logic (LTL) formulae. Spin, however, can translate such formulae into Promela syntax, with command line option -f. The translation is a never claim, encoding the Büchi acceptance condition. The formulae must then express negative properties (errors): execution sequences that satisfy the formula will be reported as correctness violations in a verification.

The operands of an LTL formula are names that represent symbolic propositions, i.e., boolean conditions on the global system state. The meaning of these conditions can be defined with macro definitions.

The temporal operators U and V are left-associative. Parentheses can be used to override this default where necessary.

EXAMPLES
Below are some examples of valid LTL formulae, as they would be passed in command-line arguments to Spin for translation into never claims.

spin -f "[] p"
spin -f "!( <> !q )"
spin -f "p U q"
spin -f "p U ([] (q U r))"

#define p       (a > b)
#define q       (len(q) < 5)

NOTES
If the Spin source itself is compiled with the preprocessor directive -DNXT, the set of temporal operators is extended with one additional unary operator: X (next). The X operator asserts the truth of the sub-formula that follows it for the next system state that is reached. The use of this operator can void the validity of the partial order reduction algorithm that is used in Spin. To show that this is not the case requires a proof that the property that is specified is closed under stuttering. Spin does not perform such checks automatically (they are not needed for LTL formulae without X operators), but it does issue a warning when the check may be needed.

SEE ALSO
macros(1), never(2), trace(2), notrace(2), condition(4), remoterefs(5).