@INPROCEEDINGS{Hustadt+Schmidt@KR2002,
 AUTHOR    = {Hustadt, U. and Schmidt, R. A.},
 YEAR      = {2002},
 TITLE     = {Scientific Benchmarking with Temporal Logic Decision Procedures},
 EDITOR    = {Fensel, D. and Giunchiglia, F. and McGuinness, D. and Williams, M.-A.},
 BOOKTITLE = {Principles of Knowledge Representation and Reasoning: Proceedings
 of the Eighth International Conference (KR 2002) [Toulouse, France, 22-25 April 2002]},
 PUBLISHER = {Morgan Kaufmann},
 PAGES     = {533-544},
 CADDRESS  = {Toulouse, France},
 CMONTH    = apr # {~22-25},
 CYEAR     = {2002},
 URL       = {Hustadt+Schmidt@KR2002.pdf},
 ABSTRACT  = {In this paper we propose a hypothesis-driven design of the
 empirical analysis of different decision procedures which we refer to
 as \emph{scientific benchmarking}.  The approach is to start by
 choosing the benchmark problems for which, on the basis of analytical
 considerations, we expect a particular decision procedure to exhibit a
 behaviour different from another decision procedure.  Then empirical
 tests are performed in order to verify the particular hypothesis
 concerning the decision procedures under consideration.  As a case
 study, we apply this methodology to compare different decision
 procedures for propositional temporal logic.  We define two classes of
 randomly generated temporal logic formulae which we use to investigate
 the behaviour of two tableaux-based temporal logic approaches using
 the Logics Workbench, a third tableaux-based approach using the
 STeP system, and temporal resolution using a new prover
 called TRP.}
}