Model Checking of Unrestricted Hierarchical State Machines
Michael Benedikt, Patrice Godefroid, and Thomas Reps
Hierarchical State Machines (HSMs) are a natural model for
representing the behavior of software systems.
In this paper, we investigate a variety of model-checking problems
for an extension of HSMs in which state machines are allowed to
call each other recursively.
(Click here to access the paper:
PostScript,
PDF.)