2.1.1.1 The formula generation algorithm

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      if n = 1 then begin
     3          p := random atomic proposition or TRUE or FALSE;
     4          return p;
     5      end
     6      else if n = 2 then begin
     7          op := random unary operator;
     8          f := RandomFormula(1);
     9          return op f;
     10     end
     11     else begin
     12         op := random unary or binary operator;
     13         if op is a unary operator then begin
     14             f := RandomFormula(n-1);
     15             return op f;
     16         end
     17         else begin
     18             x := random integer in the interval [1,n-2];
     19             f1 := RandomFormula(x);
     20             f2 := RandomFormula(n-x-1);
     21             return (f1 op f2);
     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.