Model Checking: A ComplexityTheoretic Perspective Moshe Vardi
In model checking one uses algorithmic techniques to
establish the correctness of the design with respect to a given
property. Model checking is based on a small number of
key algorithmic ideas, tying together graph theory, automata
theory, and logic. In the last few years, this area has seen a
dramatic expansion of activities. Today many companies cannot wait
to get the most advanced tools available, and many of them have formed
R&D groups to develop model checking tools and apply them to their own
designs. Unfortunately, myths abound about the computational complexity
of model checking. This talk will provide an overview of model checking
from the perspective of computational complexity and will explain why such
complexity pose a serious barrier to the broad applicability of model
checking.
