NAME
LTL

lineartime 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
Userdefined: 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 leftassociative.
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 commandline 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))"
The conditions
p
and
q
can be defined with
macro s
as:
#define p (a > b)
#define q (len(q) < 5)
elsewhere in the Promela program.
Variables
a
and
b ,
and channel name
q
must be globally declared to be visible to LTL formulae.
Remote references, as defined in
remoterefs(5), can be used indirectly, via
macro
definitions.
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 subformula 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).
