Paper: Tree-like Counterexamples in Model Checking (at LICS 2002)

Authors: Edmund M. Clarke Somesh Jha Yuan Lu Helmut Veith

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 omega-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.

BibTeX

  @InProceedings{ClarkeJhaLuVeith-TreelikeCounterexam,
    author = 	 {Edmund M. Clarke and Somesh Jha and Yuan Lu and Helmut Veith},
    title = 	 {Tree-like Counterexamples in Model Checking},
    booktitle =  {Proceedings of the Seventeenth Annual IEEE Symposium on Logic in Computer Science (LICS 2002)},
    year =	 {2002},
    month =	 {July}, 
    pages =      {19--29},
    location =   {Copenhagen, Denmark}, 
    publisher =	 {IEEE Computer Society Press}
  }