Analysis of Recursive State Machines
R. Alur, M. Benedikt, K. Etessami, P. Godefroid, T. Reps, and M. 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 and comparing their expressiveness with other
models, we focus on whether verification can be performed efficiently
for RSMs. Our first goal is to examine the verification of
linear-time properties of RSMs. We begin this study by dealing with
two key components 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(nq2) and space
O(nq), where n is the size of
the recursive machine and q is the maximum,
over all component state machines, of the minimum of the number of
entries and the number of exits of each component. From this, we
easily derive algorithms for linear time temporal logic model checking
with the same complexity in the model. We then turn to properties in
the branching time logic CTL*, and again demonstrate a
bound linear in the size of the state machine, but only for the case
of RSMs with a single exit node.
[Click here to access the paper:
PDF (via ACM Digital Library).]