Recursive state machines (RSMs) enhance the power of ordinary state
machines by allowing vertices to correspond either to ordinary states
or to potentially recursive invocations of other state machines. RSMs
can model the control flow in sequential imperative programs
containing recursive procedure calls. They can be viewed as a visual
notation extending Statecharts-like hierarchical state machines, where
concurrency is disallowed but recursion is allowed. They are also
related to various models of pushdown systems studied in the
verification and program analysis communities.
After introducing RSMs, we focus on whether state-space analysis can
be performed efficiently for RSMs. We consider the two central
problems for algorithmic analysis and model checking, namely,
reachability (is a target state reachable from initial states) and
cycle detection (is there a reachable cycle containing an accepting
state). We show that both these problems can be solved in time
O(n r^2) and space O(n r), where n is the size of the
recursive machine and r is the maximum, over all component
state machines, of the minimum of the number of entries and the number
of exits of each component. We also study the precise relationship
between RSMs and closely related models.
