The most widely used verification techniques are testing and simulation. In the case of complex, asynchronous systems, however, these techniques can cover only a limited portion of possible behaviors. A complementary verification technique is Temporal Logic Model Checking [23,28,51]. In this approach, the verified system is modeled as a finite state transition system, and the specifications are expressed in a propositional temporal logic. Then, by exhaustively exploring the state space of the state transition system, it is possible to check automatically if the specifications are satisfied. The termination of model checking is guaranteed by the finiteness of the model. One of the most important features of model checking is that, when a specification is found not to hold, a counterexample (i.e., a witness of the offending behavior of the system) is produced.
>