[Back]

E. Clarke, S. Jha, Y. Lu, H. Veith:
"Tree-Like Counterexamples in Model Cheking";
Talk: 17^th Annual IEEE Symposium on Logic in Computer Science (LIC'S02), Copenhagen, Denmark; 07-22-2002 - 07-25-2002; in: "Proceedings of the Seventeenth Annual IEEE Symposium on Logic in Computer Science (LICS' 2002)", (2002), ISBN: 0-7695-1483-9; 19 - 29.

Counterexamples for specification violations provide etngineers 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 suprisingly 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 w-regular temporal operators. (ii) We present new symbolic algorithms to generate tree-like counterexamples for ACTL specifications. (iii) Based on tree-like counterexamples we extend the abstraction refinement methodology developed recently by Clarke et al. (CAV'2000) to full ACTL. This demonstrates the conceptual simplicity and elegance of tree-like counterexamples.