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:

and the following temporal operators:

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:

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.