## Model Checking of Hierarchical State Machines

*Rajeev Alur and
Mihalis Yannakakis*
Model checking is emerging as a practical tool for detecting
logical errors in early stages of system design.
We investigate the model checking
of sequential hierarchical (nested) systems, i.e. finite state machines
whose states themselves can be other machines. This
nesting ability is common in
various software design methodologies
and is available in several commercial modeling tools.
The straightforward way to analyze a hierarchical machine is
to flatten it (thus, incurring an exponential blow up)
and apply a model checking tool on the resulting ordinary FSM.
We show that this flattening can be avoided.
We develop algorithms for verifying linear time
requirements whose complexity is polynomial in the
size of the hierarchical machine.
We address also the verification of branching time
requirements and provide efficient algorithms and matching
lower bounds.

Preliminary version appeared in
*Proceedings of the
Sixth ACM Symposium on Foundations of Software Engineering*
(FSE'98), pp. 175--188, 1998.