### Model Checking Techniques for the Analysis of Reactive Systems

Stephan Merz
Abstract
Model checking is nowadays being used routinely to design and debug reactive systems. This paper gives an overview on the theory and algorithms used for model checking, with a bias towards automata-theoretic approaches and linear-time temporal logic. We also describe elementary abstraction techniques that can be useful for large systems that cannot be directly handled by model checking.
Note
This paper was presented at a workshop on Foundations of the formal sciences in Berlin in 1998. The journal version was accepted in 1999, but appeared in print only in late 2002. I consider my other tutorial paper on model checking a better introduction to the field.
Available as:  ps.gz
Reference
@Article{merz:modelchecking-synthese,
author =  {Stephan Merz},
title =   {Model Checking Techniques for the Analysis of
Reactive Systems},
journal = {Synthese},
year =    2002,
volume =  133,
pages =   {173--201},
note =    {Special Issue \emph{Foundations of the Formal Sciences},
B.\ L{\"o}we and F.\ Rudolph (eds.)}
}


Stephan Merz