Counterexamples in Model Checking

Helmut Veith
Vienna University of Technology, Austria

Electronic mail: veith@dbai.tuwien.ac.at


Model checking is a technique for verifying that a system satisfies
its specification by representing the system as a Kripke structure,
writing the specification in a suitable temporal logic, and
algorithmically checking that the Kripke structure is a model of the
specification formula. When the model checking software detects the
violation of a specified property, it can in many cases provide the
engineer with a diagnostic counterexample.  This counterexample
exhibits the erroneous behavior and facilitates efficient debugging.
Therefore, counterexamples are considered a crucial feature in
practical applications of model checking.

In more recent work, we have used the counterexample feature of model
checking also to improve the performance of model checking algorithms
on large state spaces.  In this method, increasingly accurate
approximations of the state space are obtained by an adaptive
algorithm which analyzes counterexamples over approximate ("abstract")
state spaces.

This motivates a systematic investigation of counterexamples in model
checking.  We introduce a general framework for counterexamples, and
show that a large class of universal branching time logics based on
omega-regular operators admits counterexamples of a simple
combinatorial form similar to finite trees. Such counterexamples can
be efficiently generated by symbolic algorithms, and render the
approximation technique described above complete for important logics
such as ACTL.