Abstract
The recent emergence of heavily-optimised modal decision procedures has
lead to a number of generation methods for modal formulae.
However, the generation methods developed so far are not
satisfactory. To cope with this fact,
we propose a much improved version of one of the best-known methods,
the random CNF
_{[]m} test.
The new method drastically reduces the influence of a major
flaw of the previous method, and allows us to generate a
wider variety of problems covering much more of the input space.
This produces more interesting test sets for the current generation of
modal decision procedures.
Talk presented at IJCAR-2001 Workshop on Issues in the Design and
Experimental Evaluation of Systems for Modal and Temporal Logics,
Sienna, Italy, June 2001.