Logic in Computer Science, Symposium on (2002)
July 22, 2002 to July 25, 2002
Edmund Clarke , Carnegie Mellon University
Somesh Jha , University of Wisconsin
Yuan Lu , Broadcom COM
Helmut Veith , Technische Universität Wien
Counterexamples for specification violations provide engineers with important debugging information. Although counterexamples are considered one of the main advantages of model checking, state-of the art model checkers are restricted to relatively simple counterexamples, and surprisingly little research effort has been put into counterexamples. In this paper, we introduce a new general framework for counterexamples. The paper has three main contributions: (i) We determine the general form of ACTL counterexamples. To this end, we investigate the notion of counterexample and show that a large class of temporal logics beyond ACTL admits counterexamples with a simple tree-like transition relation. We show that the existence of tree-like counterexamples is related to a universal fragment of extended branching time logic based on !
H. Veith, E. Clarke, Y. Lu and S. Jha, "Tree-Like Counterexamples in Model Checking," Logic in Computer Science, Symposium on(LICS), Copenhagen, Denmark, 2002, pp. 19.