Model checking techniqes for the analysis of reactive systems

Stephan Merz

pp. 173-201

in: Benedikt Lowe, Florian Rudolph (eds), Foundations of the formal sciences I, Synthese 133, 2002.

Abstract

Model checking is a widely used technique that aids in the designand debugging of reactive systems. This paper gives an overview onthe theory and algorithms used for model checking, with a biastowards automata-theoretic approaches and linear-time temporallogic. We also describe elementary abstraction techniques useful forlarge systems that cannot be directly handled by model checking.