The Community for Technology Leaders
Logic in Computer Science, Symposium on (2002)
Copenhagen, Denmark
July 22, 2002 to July 25, 2002
ISSN: 1043-6871
ISBN: 0-7695-1483-9
pp: 19
Edmund Clarke , Carnegie Mellon University
Somesh Jha , University of Wisconsin
Yuan Lu , Broadcom COM
Helmut Veith , Technische Universität Wien
ABSTRACT
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 !
INDEX TERMS
null
CITATION

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.
doi:10.1109/LICS.2002.1029814
96 ms
(Ver 3.3 (11022016))