Next: , Previous: Random input generation, Up: Random input generation

#### 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.