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.