Abstract
Hierarchical state machines are finite state machines whose states themselves can be other state machines. Hierarchy is a useful construct in many modeling formalisms and tools for software design, requirements and testing.We summarize recent work on hierarchical state machines with or without concurrency. We discuss issues of expressiveness and succinctness, the complexity of basic operations (such as emptiness, equivalence etc.), and algorithmic problems in the analysis of hierarchical machines to check for their properties.
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, G.J. Holzmann, and D. Peled. An analyzer for message sequence charts. Software Concepts and Tools, 17(2):70–77, 1996.
R. Alur, S. Kannan, and M. Yannakakis. Communicating hierarchical state machines. Proc. 26th Intl. Coll. on Automata, Languages and Programming, 1999.
R. Alur, and M. Yannakakis. Model checking of hierarchical state machines. In Proc. Sixth Symp. on Foundations of Software Engineering, pp. 175–188. 1998.
R. Alur, and M. Yannakakis. Model checking of message sequence charts. In proc.10th concur., Springer Verlag, 1999.
L. Apfelbaum. Automated functional test generation. In Proc. IEEE Autotestcon Conference, 1995. See also, http://www.teradyne.com/prods/sst/product_center/t_main.html.
O. Bernholtz, M.Y. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. In Computer Aided Verification, Proc. 6th Int. Conference, LNCS 818, pages 142–155, 1994.
G. Booch, I. Jacobson, and J. Rumbaugh. Unified Modeling Language User Guide. Addison Wesley, 1997.
A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model checking. Proc. CONCUR’97, LNCS 1243, 1997.
O. Burkart and B. Steffen. Model checking for context-free processes. Proc. CONCUR’92, LNCS 630, pp. 123–137, 1992.
E.M. Clarke and E.A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proc. Workshop on Logic of Programs, LNCS 131, pages 52–71. Springer-Verlag, 1981.
C. Courcoubetis, M.Y. Vardi, P. Wolper, and M. Yannakakis. Memory efficient algorithms for the verification of temporal properties. Formal Methods in System Design, 1:275–288, 1992.
D. Drusinsky and D. Harel. On the power of bounded concurrency I: finite automata. JACM 41(3), 1994.
K. Etessami, and M. Yannakakis. From rule-based to automata-based testing. submitted, 2000.
D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8:231–274, 1987.
J. G. Henriksen, M. Mukund, K. Narayan Kumar, P. S. Thiagarajan. On message sequence graphs and finitely generated regular MSC languages. 27th Intl. Coll. on Automata, Languages and Programming, 2000.
G.J. Holzmann. The model checker SPIN. IEEE Trans. on Software Engineering, 23(5):279–295, 1997.
G.J. Holzmann, D. A. Peled, M. H. Redberg. Design tools for requirements engineering. Bell Labs Technical Journal, 2(1):86–95, 1997.
J. Hartmanis and R. E. Stearns. Algebraic Structure Theory of Sequential Machines, Prentice-Hall, 1966.
J. E. Hopcroft and J. D. Ullman. Introduction to automata theory, languages and computation. Addison-Wesley, 1979.
I. Jacobson. Object-oriented software engineering: a use case driven approach. Addison-Wesley, 1992.
F. Jahanian and A.K. Mok. A graph-theoretic approach for timing analysis and its implementation. IEEE Trans. on Computers, C-36(8):961–975, 1987.
D. Kozen. Lower bounds for natural proof systems. Proc. 18th Annual IEEE Symp. on Foundations of Computer Science, pp. 254–266, 1977.
R.P. Kurshan. Computer-aided verification of coordinating processes: the automata-theoretic approach. Princeton University Press, 1994.
N.G. Leveson, M. Heimdahl, H. Hildreth, and J.D. Reese. Requirements specification for process control systems. IEEE Trans. on Software Engineering, 20(9), 1994.
D. Lee and M. Yannakakis. Principles and Methods of Testing Finite State Machines-A Survey. Proceedings of the IEEE, 84(8), pp. 1090–1126, 1996.
K. McMillan. Symbolic model checking: An approach to the sate explosion problem. Kluwer Academic, 1993.
ITU-T Recommendation Z.120. Message Sequence Chart (MSC). 1996.
A. Pnueli. The temporal logic of programs. In Proc. of the 18th IEEE Symposium on Foundations of Computer Science, pages 46–77, 1977.
J.P. Queille and J. Sifakis. Specification and verification of concurrent programs in CESAR. Proc. of the 5th Intl. Symp. on Programming, LNCS 137, pp. 195–220, 1982.
J. Rumbaugh, M. Blaha, W. Premerlani, F. Eddy, W. Lorensen. Object-oriented modeling and design. Prentice-Hall, 1991.
E. Rudolph, J. Grabowski, P. Graubmann. Tutorial on Message Sequence Charts (MSC’96). FORTE/PSTV’96, 1996.
B. Selic, G. Gullekson, and P. T. Ward. Real-time object oriented modeling and design. J. Wiley, 1994.
M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. Proc. of the First IEEE Symp. on Logic in Computer Science, pp. 332–344, 1986.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Yannakakis, M. (2000). Hierarchical State Machines. In: van Leeuwen, J., Watanabe, O., Hagiya, M., Mosses, P.D., Ito, T. (eds) Theoretical Computer Science: Exploring New Frontiers of Theoretical Informatics. TCS 2000. Lecture Notes in Computer Science, vol 1872. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44929-9_24
Download citation
DOI: https://doi.org/10.1007/3-540-44929-9_24
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67823-6
Online ISBN: 978-3-540-44929-4
eBook Packages: Springer Book Archive