2.1.1 Random LTL formulas
The LTL formulas used by lbtt are built from
atomic propositions (with names of the form
`p'n
for some nonnegative integer n), the Boolean constants
`true' and `false',
and logical or temporal operators. lbtt supports the
following logical operators:
- logical disjunction
(`\/' as shown in output messages),
- logical conjunction
(`/\'),
- logical negation
(`!'),
- logical implication
(`->')
- logical equivalence
(`<->')
- logical “exclusive or”
(`xor')
and the following temporal operators:
- “Next time”
(`X'),
- “(Strong) Until”
(`U'),
- “Weak Until” (also known as “Unless”)
(`W'),
- “Finally” (“Eventually”)
(`<>')
- “Before”
(`B')
- “(Weak) Release”, the dual of “(Strong) Until”
(`V'),
- “Strong Release”, the dual of “Weak Until”
(`M'),
- “Globally” (“Always”, “Henceforth”)
(`[]').
See LTL formulas, for a reference on the exact semantics of these
operators.
The behavior of lbtt's random formula generation algorithm can be
adjusted with the following parameters:
- Number of nodes in the parse tree of a formula (i.e., the total number of
occurrences of propositions, Boolean constants and operators in the formula).
- Number of different atomic propositions that can be used for generating a
formula. (Note that this does not restrict the total number of atomic
propositions in the formula, nor the number of occurrences of any individual
proposition. However, none of the generated formulas will have more than this
number of different atomic propositions.)
- Priorities for the Boolean constants and atomic propositions. The priority of
a symbol determines the relative likelihood of its occurrence in a generated
formula. The higher the priority of a symbol, the more likely it is that the
symbol will occur (with respect to the other symbols) in a generated formula; a
zero priority will exclude the symbol altogether.
- Priorities for the logical and temporal operators.
Note that the priorities for atomic symbols (Boolean constants and atomic
propositions) and the priorities of the logical and temporal operators are
independent, i.e., changing the priority of an atomic symbol does not affect
the likelihood of the occurrence of any logical or temporal operator and vice
versa.
For further details, see The formula generation algorithm for a
pseudocode description of the algorithm used for generating random LTL
formulas.