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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
R. Alur and M. Yannakakis. Model checking of hierarchical state machines. In Proc. 6th ACM Symp. on Found. of Software Engineering, pages 175–188, 1998.
H. Andersen. Model checking and boolean graphs. TCS, 126(1):3–30, 1994.
T. Ball and S. Rajamani. Bebop: A symbolic model checker for boolean programs. In SPIN’2000, volume 1885 of LNCS, pages 113–130, 2000.
M. Benedikt, P. Godefroid, and T. Reps. Model checking of unrestricted hierarchical state machines. To appear in ICALP’2001.
G. Booch, I. Jacobson, and J. Rumbaugh. The Unified Modeling Language User Guide. Addison Wesley, 1997.
A. Boujjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Applications to model checking. In CONCUR’97, pages 135–150, 1997.
O. Burkart and B. Steffen. Model checking the full modal mu-calculus for infinite sequential processes. Theoretical Computer Science, 221:251–270, 1999.
J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon. Efficient algorithms for model checking pushdown systems. In Computer Aided Verification, 12th Int. Conference, volume 1855 of LNCS, pages 232–247. Springer, 2000.
A. Finkel, B. Willems, and P. Wolper. A direct symbolic approach to model checking pushdown systems. In Infinity’97 Workshop, volume 9 of Electronic Notes in Theoretical Computer Science, 1997.
D. Harel. Statecharts: a visual formalism for complex systems. Science of Computer Programming, 8:231–274, 1987.
T. Reps. Program analysis via graph reachability. Information and Software Technology, 40(11–12):701–726, 1998.
T. Reps, S. Horwitz, and S. Sagiv. Precise interprocedural dataflow analysis via graph reachability. In POPL, pages 49–61, 1995.
J. D. Ullman. Principles of Database and Knowledge-base systems. Computer Science Press, 1988.
L. G. Valiant. General context-free recognition in less than cubic time. J. of Computer and System Sc., 10:308–315, 1975.
M. Yannakakis. Graph-theoretic methods in database theory. In Proc. 9th ACM Symp. on Principles of Database Systems, pages 230–242, 1990.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Alur, R., Etessami, K., Yannakakis, M. (2001). Analysis of Recursive State Machines. In: Berry, G., Comon, H., Finkel, A. (eds) Computer Aided Verification. CAV 2001. Lecture Notes in Computer Science, vol 2102. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44585-4_18
Download citation
DOI: https://doi.org/10.1007/3-540-44585-4_18
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42345-4
Online ISBN: 978-3-540-44585-2
eBook Packages: Springer Book Archive