Analysis of recursive state machines

1 Introduction In traditional model checking, the model is a finite state machine whose vertices correspond to system states and whose edges correspond to system transitions. In this paper we consider the analysis of recursive state machines (RSMs), in which vertices can either be ordinary states or can correspond to invocations of other state machines in a potentially recursive manner. RSMs can model control flow in typical sequential imperative programming languages with recursive procedure calls. Alternatively, RSMs can be viewed as a variant of visual notations for hierarchical state machines, such as Statecharts [10] and UML [5], where concurrency is disallowed but recursion is allowed