Model Checking of Unrestricted Hierarchical State Machines
01 January 2001
Hierarchical State Machines (HSMs) are a natural model for representing the reactive behavior of complex software systems. We investigate in this paper an extension of the HSM model where state machines are allowed to call each other recursively. Such "unrestricted" HSMs can model classes of infinite state systems such as arbitrary combinations of control-flow graphs of procedures in programming languages such as C. We precisely compare the expressiveness of unrestricted HSMs with known classes of infinite state systems, namely, context-free and pushdown processes. We then discuss several verification problems on HSMs, and present original model-checking algorithms for unrestricted HSMs.