{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:54:09Z","timestamp":1762458849386},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540222613"},{"type":"electronic","value":"9783540277552"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-27755-2_15","type":"book-chapter","created":{"date-parts":[[2010,9,13]],"date-time":"2010-09-13T23:48:13Z","timestamp":1284421693000},"page":"537-558","source":"Crossref","is-referenced-by-count":20,"title":["Message Sequence Charts"],"prefix":"10.1007","author":[{"given":"Blaise","family":"Genest","sequence":"first","affiliation":[]},{"given":"Anca","family":"Muscholl","sequence":"additional","affiliation":[]},{"given":"Doron","family":"Peled","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","unstructured":"ITU-TS recommendation Z.120 (1996)"},{"key":"15_CR2","doi-asserted-by":"crossref","first-page":"304","DOI":"10.1145\/337180.337215","volume-title":"Proceedings of the 22nd International Conference on Software Engineering","author":"R. Alur","year":"2000","unstructured":"Alur, R., Etessami, K., Yannakakis, M.: Inference of Message Sequence Charts. In: Proceedings of the 22nd International Conference on Software Engineering, Limerick, Ireland, pp. 304\u2013313. ACM, New York (2000)"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"797","DOI":"10.1007\/3-540-48224-5_65","volume-title":"Automata, Languages and Programming","author":"R. Alur","year":"2001","unstructured":"Alur, R., Etessami, K., Yannakakis, M.: Realizability and verification of MSC graphs. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol.\u00a02076, pp. 797\u2013808. Springer, Heidelberg (2001)"},{"issue":"2","key":"15_CR4","first-page":"70","volume":"17","author":"R. Alur","year":"1996","unstructured":"Alur, R., Holzmann, G.H., Peled, D.A.: An analyzer for message sequence charts. Software Concepts and Tools\u00a017(2), 70\u201377 (1996)","journal-title":"Software Concepts and Tools"},{"key":"15_CR5","volume-title":"Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science (LICS 1995)","author":"R. Alur","year":"1995","unstructured":"Alur, R., Peled, D., Penczek, W.: Model-checking of causality properties. In: Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science (LICS 1995). IEEE, Los Alamitos (1995)"},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/3-540-48320-9_10","volume-title":"CONCUR\u201999. Concurrency Theory","author":"R. Alur","year":"1999","unstructured":"Alur, R., Yannakakis, M.: Model checking of message sequence charts. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol.\u00a01664, pp. 114\u2013129. Springer, Heidelberg (1999)"},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/BFb0035393","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H. Ben-Abdallah","year":"1997","unstructured":"Ben-Abdallah, H., Leue, S.: Syntactic detection of process divergence and nonlocal choice in message sequence charts. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol.\u00a01217, pp. 259\u2013274. Springer, Heidelberg (1997)"},{"key":"15_CR8","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-04558-9","volume-title":"Systems and Software Verification, Model-Checking Techniques and Tools","author":"B. Berard","year":"2001","unstructured":"Berard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, P.: Systems and Software Verification, Model-Checking Techniques and Tools. Springer, Heidelberg (2001)"},{"issue":"2","key":"15_CR9","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1145\/322374.322380","volume":"30","author":"D. Brand","year":"1983","unstructured":"Brand, D., Zafiropulo, P.: On communicating finite-state machines. Journal of the ACM\u00a030(2), 323\u2013342 (1983)","journal-title":"Journal of the ACM"},{"key":"15_CR10","volume-title":"Model Checking","author":"E. Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)"},{"volume-title":"The Book of Traces","year":"1995","key":"15_CR11","unstructured":"Diekert, V., Rozenberg, G. (eds.): The Book of Traces. World Scientific, Singapore (1995)"},{"key":"15_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/978-3-540-24727-2_15","volume-title":"Foundations of Software Science and Computation Structures","author":"B. Genest","year":"2004","unstructured":"Genest, B., Minea, M., Muscholl, A., Peled, D.: Specifying and verifying partial order properties using template MSCs. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol.\u00a02987, pp. 195\u2013210. Springer, Heidelberg (2004)"},{"key":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/3-540-45995-2_31","volume-title":"LATIN 2002: Theoretical Informatics","author":"B. Genest","year":"2002","unstructured":"Genest, B., Muscholl, A.: Pattern matching and membership for Hierarchical Message Sequence Charts. In: Rajsbaum, S. (ed.) LATIN 2002. LNCS, vol.\u00a02286, pp. 326\u2013340. Springer, Heidelberg (2002)"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"Genest, B., Muscholl, A.: The structure of local choice in High-Level Message Sequence Charts (HMSC) Internal report LIAFA (2003), Available at http:\/\/www.crans.org\/~genest\/report_lc.ps","DOI":"10.1007\/978-3-540-45187-7_21"},{"key":"15_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"657","DOI":"10.1007\/3-540-45465-9_56","volume-title":"Automata, Languages and Programming","author":"B. Genest","year":"2002","unstructured":"Genest, B., Muscholl, A., Seidl, H., Zeitoun, M.: Infinite-state High-level MSCs: Model-checking and realizability. In: Widmayer, P., Triguero, F., Morales, R., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) ICALP 2002. LNCS, vol.\u00a02380, pp. 657\u2013668. Springer, Heidelberg (2002)"},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1007\/3-540-45319-9_34","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Gunter","year":"2001","unstructured":"Gunter, E., Muscholl, A., Peled, D.: Compositional Message Sequence Charts. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 496\u2013511. Springer, Heidelberg (2001); Journal version to appear in the International Journal on Software Tools for Technology Transfer"},{"key":"15_CR17","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-19029-2","volume-title":"Come, Let\u2019s Play: Scenario-Based Programming Using LSCs and the Play-Engine","author":"D. Harel","year":"2003","unstructured":"Harel, D., Marelly, R.: Come, Let\u2019s Play: Scenario-Based Programming Using LSCs and the Play-Engine. Springer, Heidelberg (2003)"},{"key":"15_CR18","unstructured":"H\u00e9lou\u00ebt, L., Jard, C.: Conditions for synthesis of communicating automata from HMSCs. In: 5th International Workshop on Formal Methods for Industrial Critical Systems, Berlin (2000)"},{"key":"15_CR19","unstructured":"H\u00e9lou\u00ebt, L., Le Maigat, P.: Decomposition of Message Sequence Charts. In: Proceedings of the 2nd Workshop on SDL and MSC (SAM 2000), Col de Porte, Grenoble, pp. 46\u201360 (2000)"},{"key":"15_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1007\/3-540-45022-X_57","volume-title":"Automata, Languages and Programming","author":"J.G. Henriksen","year":"2000","unstructured":"Henriksen, J.G., Mukund, M., Narayan Kumar, K., Thiagarajan, P.: On Message Sequence Graphs and finitely generated regular MSC languages. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol.\u00a01853, pp. 675\u2013686. Springer, Heidelberg (2000)"},{"key":"15_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/3-540-44612-5_36","volume-title":"Mathematical Foundations of Computer Science 2000","author":"J.G. Henriksen","year":"2000","unstructured":"Henriksen, J.G., Mukund, M., Narayan Kumar, K., Thiagarajan, P.: Regular collections of Message Sequence Charts. In: Nielsen, M., Rovan, B. (eds.) MFCS 2000. LNCS, vol.\u00a01893, pp. 405\u2013414. Springer, Heidelberg (2000)"},{"key":"15_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/3-540-45841-7_40","volume-title":"STACS 2002","author":"D. Kuske","year":"2002","unstructured":"Kuske, D.: A Further Step towards a Theory of Regular MSC Languages. In: Alt, H., Ferreira, A. (eds.) STACS 2002. LNCS, vol.\u00a02285, pp. 489\u2013500. Springer, Heidelberg (2002)"},{"key":"15_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/3-540-45694-5_13","volume-title":"CONCUR 2002 - Concurrency Theory","author":"M. Lohrey","year":"2002","unstructured":"Lohrey, M.: Safe realizability of High-level Message Sequence Charts. In: Brim, L., Jan\u010dar, P., K\u0159et\u00ednsk\u00fd, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol.\u00a02421, pp. 177\u2013192. Springer, Heidelberg (2002)"},{"key":"15_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"809","DOI":"10.1007\/3-540-48224-5_66","volume-title":"Automata, Languages and Programming","author":"P. Madhusudan","year":"2001","unstructured":"Madhusudan, P.: Reasoning about sequential and branching behaviours of Message Sequence Graphs. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol.\u00a02076, pp. 809\u2013820. Springer, Heidelberg (2001)"},{"key":"15_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/978-3-540-45187-7_20","volume-title":"CONCUR 2003 - Concurrency Theory","author":"M. Mukund","year":"2003","unstructured":"Mukund, M., Narayan Kumar, K., Thiagarajan, P.S.: Netcharts: bridging the gap between HMSCs and executable specifications. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol.\u00a02761, pp. 296\u2013310. Springer, Heidelberg (2003)"},{"key":"15_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"523","DOI":"10.1007\/3-540-45841-7_43","volume-title":"STACS 2002","author":"R. Morin","year":"2002","unstructured":"Morin, R.: Recognizable Sets of Message Sequence Charts. In: Alt, H., Ferreira, A. (eds.) STACS 2002. LNCS, vol.\u00a02285, pp. 523\u2013540. Springer, Heidelberg (2002)"},{"key":"15_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/3-540-48340-3_8","volume-title":"Mathematical Foundations of Computer Science 1999","author":"A. Muscholl","year":"1999","unstructured":"Muscholl, A., Peled, D.: Message sequence graphs and decision problems on Mazurkiewicz traces. In: Kuty\u0142owski, M., Wierzbicki, T., Pacholski, L. (eds.) MFCS 1999. LNCS, vol.\u00a01672, pp. 81\u201391. Springer, Heidelberg (1999)"},{"key":"15_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/BFb0053553","volume-title":"Foundations of Software Science and Computation Structures","author":"A. Muscholl","year":"1998","unstructured":"Muscholl, A., Peled, D., Su, Z.: Deciding properties of Message Sequence Charts. In: Nivat, M. (ed.) FOSSACS 1998. LNCS, vol.\u00a01378, pp. 226\u2013242. Springer, Heidelberg (1998)"},{"key":"15_CR29","doi-asserted-by":"crossref","unstructured":"Peled, D.: Specification and verification of Message Sequence Charts. In: Proceedings of Formal Techniques for Distributed System Development, FORTE\/PSTV 2000, Pisa, Italy, pp. 139\u2013154 (2000)","DOI":"10.1007\/978-0-387-35533-7_9"},{"key":"15_CR30","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1145\/587051.587077","volume-title":"Proceedings of SIGSOFT 2002\/FSE-10","author":"B. Sengupta","year":"2002","unstructured":"Sengupta, B., Cleaveland, R.: Triggered Message Sequence Charts. In: Proceedings of SIGSOFT 2002\/FSE-10, pp. 167\u2013176. ACM Press, New York (2002)"}],"container-title":["Lecture Notes in Computer Science","Lectures on Concurrency and Petri Nets"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-27755-2_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,3]],"date-time":"2023-06-03T04:39:52Z","timestamp":1685767192000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-27755-2_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540222613","9783540277552"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-27755-2_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}