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 !
Citation:
Edmund Clarke, Somesh Jha, Yuan Lu, Helmut Veith, "Tree-Like Counterexamples in Model Checking," lics, pp.19, 17th Annual IEEE Symposium on Logic in Computer Science (LICS'02), 2002