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.

© Kluwer 2002

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.)}
}