Analysis of Recursive State Machines

Rajeev Alur, Kousha Etessami, Mihalis Yannakakis

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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 θ (2) and space O(n θ), where n is the size of the recursive machine and θ 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.
Original languageEnglish
Title of host publicationComputer Aided Verification
Subtitle of host publication13th International Conference, CAV 2001, Paris, France, July 18-22, 2001, Proceedings
PublisherSpringer Berlin Heidelberg
Pages207-220
Number of pages14
Volume2102
ISBN (Electronic)978-3-540-44585-2
ISBN (Print)978-3-540-42345-4
DOIs
Publication statusPublished - 2001

Fingerprint

Dive into the research topics of 'Analysis of Recursive State Machines'. Together they form a unique fingerprint.

Cite this