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.