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.
