{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,7]],"date-time":"2025-11-07T13:13:19Z","timestamp":1762521199066},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540664253"},{"type":"electronic","value":"9783540483205"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48320-9_10","type":"book-chapter","created":{"date-parts":[[2007,11,15]],"date-time":"2007-11-15T08:52:42Z","timestamp":1195116762000},"page":"114-129","source":"Crossref","is-referenced-by-count":135,"title":["Model Checking of Message Sequence Charts"],"prefix":"10.1007","author":[{"given":"Rajeev","family":"Alur","sequence":"first","affiliation":[]},{"given":"Mihalis","family":"Yannakakis","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,4,19]]},"reference":[{"issue":"2","key":"10_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":"10_CR2","doi-asserted-by":"crossref","unstructured":"R. Alur and M. Yannakakis. Model checking of hierarchical state machines. In Proc. Sixth ACM FSE, 175\u2013188, 1998.","DOI":"10.1145\/288195.288305"},{"key":"10_CR3","unstructured":"G. Booch, I. Jacobson, and J. Rumbaugh. Unified Modeling Language User Guide. Addison Wesley, 1997."},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"H. Ben-Abdallah and S. Leue. Syntactic detection of process divergence and nonlocal choice in message sequence charts. In Proc. of TACAS. 1997.","DOI":"10.1007\/BFb0035393"},{"key":"10_CR5","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, 1981."},{"issue":"6","key":"10_CR6","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1109\/6.499951","volume":"33","author":"E. M. Clarke","year":"1996","unstructured":"E. M. Clarke and R. P. Kurshan. Computer-aided verification. IEEE Spectrum, 33(6):61\u201367, 1996.","journal-title":"IEEE Spectrum"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"J. Feigenbaum, J. A. Kahn, and C. Lund. Complexity results for pomset languages. In Proc. CAV, 1991.","DOI":"10.1007\/3-540-55179-4_33"},{"key":"10_CR8","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"},{"issue":"2","key":"10_CR9","first-page":"63","volume":"17","author":"G. J. Holzmann","year":"1996","unstructured":"G. J. Holzmann. Early fault detection tools. Software Concepts and Tools, 17(2):63\u201369, 1996.","journal-title":"Software Concepts and Tools"},{"issue":"5","key":"10_CR10","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":"10_CR11","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, and M. H. Redberg. Design tools for for requirements engineering. Lucent Bell Labs Technical Journal, 2(1):86\u201395, 1997.","journal-title":"Lucent Bell Labs Technical Journal"},{"key":"10_CR12","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":"10_CR13","doi-asserted-by":"crossref","unstructured":"P. Ladkin and S. Leue. Interpreting message flow graphs. Formal Aspects of Computing, 3, 1994.","DOI":"10.1007\/BF01211629"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"V. Levin, and D. Peled. Verification of message sequence charts via template matching. In Proc. TAPSOFT, 1997.","DOI":"10.1007\/BFb0030632"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"A. Muscholl, D. Peled, and Z. Su. Deciding properties of message sequence charts. In Found. of Software Science and Computation Structures, 1998.","DOI":"10.1007\/BFb0053553"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"S. Mauw and M. A. Reniers. An algebraic semantics of basic message sequence charts. Computer Journal, 37, 1994.","DOI":"10.1093\/comjnl\/37.4.269"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"V. R. Pratt. Modeling concurrency with partial orders. International Journal of Parallel Programming, 15(1), 1986.","DOI":"10.1007\/BF01379149"},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"E. Rudolph, P. Graubmann, and J. Gabowski. Tutorial on message sequence charts. In Computer Networks and ISDN Systems, volume 28. 1996.","DOI":"10.1016\/0169-7552(95)00122-0"},{"key":"10_CR19","unstructured":"B. Selic, G. Gullekson, and P. T. Ward. Real-time object oriented modeling and design. J. Wiley, 1994."},{"key":"10_CR20","unstructured":"M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. First LICS, pages 332\u2013344, 1986."}],"container-title":["Lecture Notes in Computer Science","CONCUR\u201999 Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48320-9_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,4]],"date-time":"2019-05-04T09:06:31Z","timestamp":1556960791000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48320-9_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664253","9783540483205"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-48320-9_10","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}