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.

(Click here to access the paper.)