## Analysis of Recursive State Machines

*Rajeev Alur, Kousha Etessami, and Mihalis Yannakakis*
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 accept state). We
show that both these problems can be solved in time O(n theta^2),
where n is the size of the recursive machine and
theta 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 like pushdown systems, and show that our algorithms
allow more efficient analysis than translating to pushdown systems and
applying known algorithms for pushdown systems.

*Proceedings of the
13th International
Conference on Computer-Aided Verification*
(CAV'01), 2001.