{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:54:24Z","timestamp":1762458864179},"publisher-location":"Berlin, Heidelberg","reference-count":43,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540210023"},{"type":"electronic","value":"9783540399100"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-39910-0_3","type":"book-chapter","created":{"date-parts":[[2011,1,14]],"date-time":"2011-01-14T08:05:40Z","timestamp":1294992340000},"page":"42-66","source":"Crossref","is-referenced-by-count":5,"title":["Formal Analysis of Hierarchical State Machines"],"prefix":"10.1007","author":[{"given":"Rajeev","family":"Alur","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"R. Alur, K. Etessami, and M. Yannakakis. Analysis of recursive state machines. In Proc. of the 13th International Conference on Computer Aided Verification, LNCS 2102, pages 207-220. Springer, 2001.","DOI":"10.1007\/3-540-44585-4_18"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"R. Alur and R. Grosu. Modular refinement of hierarchic reactive machines. In Proceedings of the 27th Annual ACM Symposium on Principles of Programming Languages, pages 390-402, 2000.","DOI":"10.1145\/325694.325746"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"R. Alur, R. Grosu, and M. McDougall. Efficient reachability analysis of hierarchical reactive machines. In Computer Aided Verification, 12th International Conference, LNCS 1855, pages 280-295. Springer, 2000.","DOI":"10.1007\/10722167_23"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"R. Alur, S. Kannan, and M. Yannakakis. Communicating hierarchical state machines. In Automata, Languages and Programming, 26th International Colloquium, pages 169-178. Springer, 1999.","DOI":"10.1007\/3-540-48523-6_14"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"R. Alur, S. La Torre, and P. Madhusudan. Modular strategies for recursive game graphs. In TACAS\u201903: Ninth International Conference on Tools and Algorithms for the Construction and Analysis of Software, LNCS 2619, pages 363-378, 2003.","DOI":"10.1007\/3-540-36577-X_26"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"R. Alur, M. McDougall, and Z. Yang. Exploiting behavioral hierarchy for efficient model checking. In Computer Aided Verification, 14th International Conference, LNCS 2404, pages 338-342. Springer, 2002.","DOI":"10.1007\/3-540-45657-0_25"},{"issue":"3","key":"3_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/503502.503503","volume":"23","author":"R Alur","year":"2001","unstructured":"R. Alur and M. Yannakakis. Model checking of hierarchical state machines. ACM Transactions on Programming Languages and Systems, 23(3):1\u201331, 2001.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"T. Ball and S. Rajamani. Bebop: A symbolic model checker for boolean programs. In SPIN 2000 Workshop on Model Checking of Software, LNCS 1885, pages 113-130. Springer, 2000.","DOI":"10.1007\/10722468_7"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"T. Ball and S. Rajamani. The SLAM toolkit. In Computer Aided Verification, 13th International Conference, 2001.","DOI":"10.1007\/3-540-44585-4_25"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"G. Behrmann, K. Larsen, H. Andersen, H. Hulgaard, and J. Lind-Nielsen. Verification of hierarchical state\/event systems using reusability and compositionality. In TACAS\u2019 99: Fifth International Conference on Tools and Algorithms for the Construction and Analysis of Software, LNCS 1579, pages 163-177. Springer, 1999.","DOI":"10.1007\/3-540-49059-0_12"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"M. Benedikt, P. Godefroid, and T. Reps. Model checking of unrestricted hierarchical state machines. In Automata, Languages and Programming, 28th International Colloquium, volume LNCS 2076, pages 652-666. Springer, 2001.","DOI":"10.1007\/3-540-48224-5_54"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proceedings of the 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 193-207, 1999.","DOI":"10.21236\/ADA360973"},{"key":"3_CR13","unstructured":"G. Booch, I. Jacobson, and J. Rumbaugh. Unified Modeling Language User Guide. Addison Wesley, 1997."},{"key":"3_CR14","unstructured":"A. Boujjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Applications to model checking. In CONCUR\u201997: Concurrency Theory, Eighth International Conference, LNCS 1243, pages 135-150. Springer, 1997."},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"R. Brayton, G. Hachtel, A. Sangiovanni-Vincentelli, F. Somenzi, A. Aziz, S. Cheng, S. Edwards, S. Khatri, Y. Kukimoto, A. Pardo, S. Qadeer, R. Ranjan, S. Sarwary, T. Shiple, G. Swamy, and T. Villa. VIS: A system for verification and synthesis. In Proceedings of the Eighth International Conference on Computer Aided Verification, LNCS 1102, pages 428-432. Springer-Verlag, 1996.","DOI":"10.1007\/3-540-61474-5_95"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"R. Bryant. Graph-based algorithms for boolean-function manipulation. IEEE Transactions on Computers, C-35(8), 1986.","DOI":"10.1109\/TC.1986.1676819"},{"issue":"2","key":"3_CR17","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J Burch","year":"1992","unstructured":"J. Burch, E. Clarke, D. Dill, L. Hwang, and K. McMillan. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142\u2013170, 1992.","journal-title":"Information and Computation"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"O. Burkart and B. Steffen. Model checking for context-free processes. In CONCUR\u201992: Concurrency Theory, Third International Conference, LNCS 630, pages 123-137. Springer, 1992.","DOI":"10.1007\/BFb0084787"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"A. Chakrabarti, L. de Alfaro, T. Henzinger, M. Jurdzinski, and F. Mang. Interface compatibility checking for software modules. In Proceedings of the 14th International Conference on Computer-Aided Verification, LNCS 2404, pages 428-441. Springer, 2002.","DOI":"10.1007\/3-540-45657-0_35"},{"issue":"7","key":"3_CR20","doi-asserted-by":"publisher","first-page":"498","DOI":"10.1109\/32.708566","volume":"24","author":"W Chan","year":"1998","unstructured":"W. Chan, R. Anderson, P. Beame, S. Burns, F. Modugno, D. Notkin, and J. Reese. Model checking large software specifications. IEEE Transactions on Software Engineering, 24(7):498\u2013519, 1998.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"E. Clarke and E. 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.","DOI":"10.1007\/BFb0025774"},{"key":"3_CR22","unstructured":"E. Clarke, O. Grumberg, and D. Peled. Model checking. MIT Press, 2000."},{"issue":"6","key":"3_CR23","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1109\/6.499951","volume":"33","author":"E Clarke","year":"1996","unstructured":"E. Clarke and R. Kurshan. Computer-aided verification. IEEE Spectrum, 33(6):61\u201367, 1996.","journal-title":"IEEE Spectrum"},{"key":"3_CR24","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C Courcoubetis","year":"1992","unstructured":"C. Courcoubetis, M. 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"},{"issue":"3","key":"3_CR25","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1145\/176584.176587","volume":"41","author":"D Drusinsky","year":"1994","unstructured":"D. Drusinsky and D. Harel. On the power of bounded concurrency I: finite automata. Journal of the ACM, 41(3):517\u2013539, 1994.","journal-title":"Journal of the ACM"},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon. Efficient algorithms for model checking pushdown systems. In Computer Aided Verification, 12th International Conference, LNCS 1855, pages 232-247. Springer, 2000.","DOI":"10.1007\/10722167_20"},{"key":"3_CR27","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":"3_CR28","doi-asserted-by":"crossref","unstructured":"T. Henzinger, R. Jhala, R. Majumdar, G. Necula, G. Sutre, and W. Weimer. Temporal-safety proofs for systems code. In CAV 02: Proc. of 14th Conf. on Computer Aided Verification, LNCS 2404, pages 526-538. Springer, 2002.","DOI":"10.1007\/3-540-45657-0_45"},{"key":"3_CR29","unstructured":"G. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall, 1991."},{"issue":"5","key":"3_CR30","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G Holzmann","year":"1997","unstructured":"G. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279\u2013295, 1997.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"3_CR31","unstructured":"J. Hopcroft and J. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 1979."},{"issue":"2","key":"3_CR32","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1145\/333979.333987","volume":"47","author":"O Kupferman","year":"2000","unstructured":"O. Kupferman, M. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. Journal of the ACM, 47(2):312\u2013360, 2000.","journal-title":"Journal of the ACM"},{"key":"3_CR33","doi-asserted-by":"crossref","unstructured":"R. Kurshan. Computer-aided Verification of Coordinating Processes: the automata-theoretic approach. Princeton University Press, 1994.","DOI":"10.1515\/9781400864041"},{"key":"3_CR34","doi-asserted-by":"crossref","unstructured":"S. La Torre, M. Napoli, M. Parento, and G. Parlato. Hierarchical and recursive state machines with context dependent properties. In Automata, Languages and Programming, 30th International Colloquium, LNCS 2719, pages 776-789, 2003.","DOI":"10.1007\/3-540-45061-0_61"},{"issue":"9","key":"3_CR35","doi-asserted-by":"publisher","first-page":"684","DOI":"10.1109\/32.317428","volume":"20","author":"N Leveson","year":"1994","unstructured":"N. Leveson, M. Heimdahl, H. Hildreth, and J. Reese. Requirements specification for process control systems. IEEE Transactions on Software Engineering, 20(9):684\u2013707, 1994.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"3_CR36","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli. Checking that finite-state concurrent programs satisfy their linear specification. In Proceedings of the 12th ACM Symposium on Principles of Programming Languages, pages 97-107, 1985.","DOI":"10.1145\/318593.318622"},{"key":"3_CR37","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. The temporal logic of reactive and concurrent systems: Specification. Springer-verlag, 1991.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"3_CR38","doi-asserted-by":"crossref","unstructured":"K. McMillan. Symbolic model checking: an approach to the state explosion problem. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"3_CR39","doi-asserted-by":"crossref","unstructured":"A. Pnueli. The temporal logic of programs. In Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, pages 46-77, 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"3_CR40","unstructured":"B. Selic, G. Gullekson, and P. Ward. Real-time object oriented modeling and design. J. Wiley, 1994."},{"key":"3_CR41","doi-asserted-by":"crossref","unstructured":"W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 133-191. Elsevier Science Publishers, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"issue":"1","key":"3_CR42","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M Vardi","year":"1994","unstructured":"M. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1\u201337, 1994.","journal-title":"Information and Computation"},{"issue":"2","key":"3_CR43","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1006\/inco.2000.2894","volume":"164","author":"I Walukiewicz","year":"2001","unstructured":"I. Walukiewicz. Pushdown processes: Games and model-checking. Information and Computation, 164(2):234\u2013263, 2001.","journal-title":"Information and Computation"}],"container-title":["Lecture Notes in Computer Science","Verification: Theory and Practice"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-39910-0_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T21:07:15Z","timestamp":1559941635000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-39910-0_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540210023","9783540399100"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-39910-0_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}