{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,7]],"date-time":"2025-06-07T17:41:24Z","timestamp":1749318084044},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540678236"},{"type":"electronic","value":"9783540449294"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44929-9_24","type":"book-chapter","created":{"date-parts":[[2007,5,5]],"date-time":"2007-05-05T09:20:53Z","timestamp":1178356853000},"page":"315-330","source":"Crossref","is-referenced-by-count":21,"title":["Hierarchical State Machines"],"prefix":"10.1007","author":[{"given":"Mihalis","family":"Yannakakis","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,8,24]]},"reference":[{"issue":"2","key":"24_CR1","first-page":"70","volume":"17","author":"R. Alur","year":"1996","unstructured":"R. Alur, G.J. Holzmann, and D. Peled. An analyzer for message sequence charts. Software Concepts and Tools, 17(2):70\u201377, 1996.","journal-title":"Software Concepts and Tools"},{"key":"24_CR2","doi-asserted-by":"crossref","unstructured":"R. Alur, S. Kannan, and M. Yannakakis. Communicating hierarchical state machines. Proc. 26th Intl. Coll. on Automata, Languages and Programming, 1999.","DOI":"10.1007\/3-540-48523-6_14"},{"key":"24_CR3","doi-asserted-by":"crossref","unstructured":"R. Alur, and M. Yannakakis. Model checking of hierarchical state machines. In Proc. Sixth Symp. on Foundations of Software Engineering, pp. 175\u2013188. 1998.","DOI":"10.1145\/288195.288305"},{"key":"24_CR4","doi-asserted-by":"crossref","unstructured":"R. Alur, and M. Yannakakis. Model checking of message sequence charts. In proc.10th concur., Springer Verlag, 1999.","DOI":"10.1007\/3-540-48320-9_10"},{"key":"24_CR5","unstructured":"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 ."},{"key":"24_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1007\/3-540-58179-0_50","volume-title":"Computer Aided Verification, Proc. 6th Int. Conference","author":"O. Bernholtz","year":"1994","unstructured":"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\u2013155, 1994."},{"key":"24_CR7","unstructured":"G. Booch, I. Jacobson, and J. Rumbaugh. Unified Modeling Language User Guide. Addison Wesley, 1997."},{"key":"24_CR8","series-title":"Lect Notes Comput Sci","volume-title":"Proc. CONCUR\u201997","author":"A. Bouajjani","year":"1997","unstructured":"A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model checking. Proc. CONCUR\u201997, LNCS 1243, 1997."},{"key":"24_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/BFb0084787","volume-title":"Proc. CONCUR\u201992","author":"O. Burkart","year":"1992","unstructured":"O. Burkart and B. Steffen. Model checking for context-free processes. Proc. CONCUR\u201992, LNCS 630, pp. 123\u2013137, 1992."},{"key":"24_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Proc. Workshop on Logic of Programs","author":"E.M. Clarke","year":"1981","unstructured":"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\u201371. Springer-Verlag, 1981."},{"key":"24_CR11","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C. Courcoubetis","year":"1992","unstructured":"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\u2013288, 1992.","journal-title":"Formal Methods in System Design"},{"key":"24_CR12","doi-asserted-by":"crossref","unstructured":"D. Drusinsky and D. Harel. On the power of bounded concurrency I: finite automata. JACM 41(3), 1994.","DOI":"10.1145\/176584.176587"},{"key":"24_CR13","doi-asserted-by":"crossref","unstructured":"K. Etessami, and M. Yannakakis. From rule-based to automata-based testing. submitted, 2000.","DOI":"10.1007\/978-0-387-35533-7_4"},{"key":"24_CR14","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D. Harel","year":"1987","unstructured":"D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8:231\u2013274, 1987.","journal-title":"Science of Computer Programming"},{"key":"24_CR15","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1007\/3-540-45022-X_57"},{"issue":"5","key":"24_CR16","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"G.J. Holzmann. The model checker SPIN. IEEE Trans. on Software Engineering, 23(5):279\u2013295, 1997.","journal-title":"IEEE Trans. on Software Engineering"},{"issue":"1","key":"24_CR17","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1002\/bltj.2034","volume":"2","author":"G.J. Holzmann","year":"1997","unstructured":"G.J. Holzmann, D. A. Peled, M. H. Redberg. Design tools for requirements engineering. Bell Labs Technical Journal, 2(1):86\u201395, 1997.","journal-title":"Bell Labs Technical Journal"},{"key":"24_CR18","unstructured":"J. Hartmanis and R. E. Stearns. Algebraic Structure Theory of Sequential Machines, Prentice-Hall, 1966."},{"key":"24_CR19","unstructured":"J. E. Hopcroft and J. D. Ullman. Introduction to automata theory, languages and computation. Addison-Wesley, 1979."},{"key":"24_CR20","unstructured":"I. Jacobson. Object-oriented software engineering: a use case driven approach. Addison-Wesley, 1992."},{"issue":"8","key":"24_CR21","doi-asserted-by":"publisher","first-page":"961","DOI":"10.1109\/TC.1987.5009519","volume":"36","author":"F. Jahanian","year":"1987","unstructured":"F. Jahanian and A.K. Mok. A graph-theoretic approach for timing analysis and its implementation. IEEE Trans. on Computers, C-36(8):961\u2013975, 1987.","journal-title":"IEEE Trans. on Computers"},{"key":"24_CR22","doi-asserted-by":"crossref","unstructured":"D. Kozen. Lower bounds for natural proof systems. Proc. 18th Annual IEEE Symp. on Foundations of Computer Science, pp. 254\u2013266, 1977.","DOI":"10.1109\/SFCS.1977.16"},{"key":"24_CR23","doi-asserted-by":"crossref","unstructured":"R.P. Kurshan. Computer-aided verification of coordinating processes: the automata-theoretic approach. Princeton University Press, 1994.","DOI":"10.1515\/9781400864041"},{"key":"24_CR24","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1109\/32.317428"},{"issue":"8","key":"24_CR25","doi-asserted-by":"publisher","first-page":"1090","DOI":"10.1109\/5.533956","volume":"84","author":"D. Lee","year":"1996","unstructured":"D. Lee and M. Yannakakis. Principles and Methods of Testing Finite State Machines-A Survey. Proceedings of the IEEE, 84(8), pp. 1090\u20131126, 1996.","journal-title":"Proceedings of the IEEE"},{"key":"24_CR26","doi-asserted-by":"crossref","unstructured":"K. McMillan. Symbolic model checking: An approach to the sate explosion problem. Kluwer Academic, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"24_CR27","unstructured":"ITU-T Recommendation Z.120. Message Sequence Chart (MSC). 1996."},{"key":"24_CR28","doi-asserted-by":"crossref","unstructured":"A. Pnueli. The temporal logic of programs. In Proc. of the 18th IEEE Symposium on Foundations of Computer Science, pages 46\u201377, 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"24_CR29","series-title":"Lect Notes Comput Sci","first-page":"195","volume-title":"Proc. of the 5th Intl. Symp. on Programming","author":"J.P. Queille","year":"1982","unstructured":"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\u2013220, 1982."},{"key":"24_CR30","unstructured":"J. Rumbaugh, M. Blaha, W. Premerlani, F. Eddy, W. Lorensen. Object-oriented modeling and design. Prentice-Hall, 1991."},{"key":"24_CR31","doi-asserted-by":"crossref","unstructured":"E. Rudolph, J. Grabowski, P. Graubmann. Tutorial on Message Sequence Charts (MSC\u201996). FORTE\/PSTV\u201996, 1996.","DOI":"10.1016\/0169-7552(95)00122-0"},{"key":"24_CR32","unstructured":"B. Selic, G. Gullekson, and P. T. Ward. Real-time object oriented modeling and design. J. Wiley, 1994."},{"key":"24_CR33","unstructured":"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\u2013344, 1986."}],"container-title":["Lecture Notes in Computer Science","Theoretical Computer Science: Exploring New Frontiers of Theoretical Informatics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44929-9_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,11]],"date-time":"2023-05-11T14:37:59Z","timestamp":1683815879000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44929-9_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540678236","9783540449294"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/3-540-44929-9_24","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}