@INPROCEEDINGS{HustadtSchmidt02b,
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)},
PUBLISHER = {Morgan Kaufmann},
PAGES = {533--544},
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 
\textsl{STeP} system, and temporal resolution using a new prover 
called \textsl{TRP}.}
}