Previous: Random LTL formulas, Up: Random LTL formulas

`lbtt` uses an algorithm similar to the one outlined in
[DGV99]
for generating random LTL formulas. The algorithm can be described in
pseudocode as follows:

1 function RandomFormula(n: Integer) : LtlFormula; 2 ifn= 1 then begin 3p:= random atomic proposition or TRUE or FALSE; 4 returnp; 5 end 6 else ifn= 2 then begin 7op:= random unary operator; 8f:= RandomFormula(1); 9 returnopf; 10 end 11 else begin 12op:= random unary or binary operator; 13 ifopis a unary operator then begin 14f:= RandomFormula(n-1); 15 returnopf; 16 end 17 else begin 18x:= random integer in the interval [1,n-2]; 19f1:= RandomFormula(x); 20f2:= RandomFormula(n-x-1); 21 return (f1opf2); 22 end; 23 end; 24 end;

Each invocation of the algorithm returns an LTL formula with `n`
nodes in the formula parse tree. The behavior of the algorithm can be adjusted
by giving values for the parameters `n` (the number of nodes in the
formula parse tree),
|AP|
(the number of different atomic propositions), and
pri(`symbol`)
(the priorities for the different symbols).

In `lbtt`'s implementation of the above algorithm, the priority of a
symbol determines the probability with which the symbol is chosen
into a generated formula each time line 3, 7 or 12 of the algorithm is
executed. For Boolean constants
``true`' and ``false`'
(line 3 of the algorithm), the probability is given by the equation

pri(`CONSTANT`) / (pri(AP) + pri(``true`') + pri(``false`'))

where `CONSTANT` is either
``true`' or ``false`',
and
pri(AP)
is the total priority of all atomic propositions.

The probability of choosing a particular atomic proposition into a formula (line 3) is

pri(AP) / (|AP| * (pri(AP) + pri(``true`') + pri(``false`'))),

where |AP| and pri(AP) are as defined above.

Line 7 of the algorithm concerns choosing a unary operator
(``!`', ``X`', ``<>`' or ``[]`')
into a formula. Here the probability of choosing the unary operator
`op`
is given by the equation

pri(`op`) / Sum (pri(`op'`)),

where
`op'`
ranges over all unary operators.

Finally, at line 12 of the algorithm, the probability of choosing the (unary or
binary) operator
`op`
into the formula is

pri(`op`) / Sum (pri(`op'`)),

where
`op'`
ranges over all unary and binary
operators (``!`', ``\/`', ``/\`', ``->`', ``<->`', ``xor`',
``X`', ``U`', ``W`', ``<>`', ``B`', ``V`', ``M`',
``[]`').

An analysis of this algorithm is included in an appendix of
[Tau00].
The analysis shows how to use the operator priorities to calculate the
expected number of occurrences of an operator in a randomly generated
formula. `lbtt` can optionally compute the expected operator
distribution for a given combination of operator priorities; see the
``--showoperatordistribution`' command line option
(see ``--showoperatordistribution`' command line option)
for more information.

See also the web page

<http://www.tcs.hut.fi/Software/lbtt/formulaoptions.php>
for an interface to a small database for adjusting the operator priorities
towards certain simple distributions.