{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:53:44Z","timestamp":1762458824959},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540261896"},{"type":"electronic","value":"9783540320326"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11495628_3","type":"book-chapter","created":{"date-parts":[[2010,7,13]],"date-time":"2010-07-13T12:03:05Z","timestamp":1279022585000},"page":"43-65","source":"Crossref","is-referenced-by-count":8,"title":["Deciding Properties of Message Sequence Charts"],"prefix":"10.1007","author":[{"given":"Anca","family":"Muscholl","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Doron","family":"Peled","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","first-page":"304","volume-title":"Proc.\u00a0of the 22nd Int.\u00a0Conf.\u00a0on Software Engineering","author":"R. Alur","year":"2000","unstructured":"Alur, R., Etessami, K., Yannakakis, M.: Inference of message sequence charts. In: Proc.\u00a0of the 22nd Int.\u00a0Conf.\u00a0on Software Engineering, pp. 304\u2013313. ACM Press, New York (2000)"},{"key":"3_CR2","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":"3_CR3","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":"3_CR4","doi-asserted-by":"crossref","unstructured":"Alur, R., Peled, D., Penczek, W.: Model Checking of Causality Properties. In: Proc.\u00a0of Logic in Computer Science (LICS 1995), pp. 90\u2013100 (1995)","DOI":"10.1109\/LICS.1995.523247"},{"key":"3_CR5","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":"3_CR6","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-Abdulla","year":"1997","unstructured":"Ben-Abdulla, H., Leue, S.: Symbolic Detection of Process Divergence and Non-local Choice in Message Sequence Charts. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol.\u00a01217, pp. 259\u2013274. Springer, Heidelberg (1997)"},{"key":"3_CR7","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/10722167_20","volume-title":"Computer Aided Verification","author":"J. Esparza","year":"2000","unstructured":"Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithms for model checking pushdown systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 232\u2013247. Springer, Heidelberg (2000)"},{"key":"3_CR9","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":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/978-3-540-31980-1_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B. Genest","year":"2005","unstructured":"Genest, B.: Compositional Message Sequence Charts (CMSCs) are better to Implement than MSCs. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 429\u2013444. Springer, Heidelberg (2005)"},{"key":"#cr-split#-3_CR11.1","doi-asserted-by":"crossref","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);","DOI":"10.1007\/3-540-45319-9_34"},{"key":"#cr-split#-3_CR11.2","unstructured":"Journal version. International Journal on Software Tools for Technology Transfer (STTT)\u00a05(1), 78\u201389 (2003)"},{"key":"3_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"537","DOI":"10.1007\/978-3-540-27755-2_15","volume-title":"Lectures on Concurrency and Petri Nets","author":"B. Genest","year":"2004","unstructured":"Genest, B., Muscholl, A., Peled, D.: Message sequence charts. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol.\u00a03098, pp. 537\u2013558. Springer, Heidelberg (2004)"},{"key":"3_CR13","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":"3_CR14","volume-title":"Design and Validation of Computer Protocols","author":"G. Holzmann","year":"1992","unstructured":"Holzmann, G.: Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs (1992)"},{"key":"3_CR15","unstructured":"ITU-T Recommendation Z.120, Message Sequence Chart, MSC (1996)"},{"key":"3_CR16","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":"3_CR17","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.S.: 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":"3_CR18","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.S.: Regular collections of message sequence charts. In: Nielsen, M., Rovan, B. (eds.) MFCS 2000. LNCS, vol.\u00a01893, pp. 405\u2013414. Springer, Heidelberg (2000)"},{"key":"3_CR19","volume-title":"Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach","author":"R.P. Kurshan","year":"1994","unstructured":"Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton (1994)"},{"issue":"187","key":"3_CR20","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1016\/S0890-5401(03)00123-8","volume":"1","author":"D. Kuske","year":"2003","unstructured":"Kuske, D.: Regular sets of infinite message sequence charts. Information and Computation\u00a0(187), 80\u2013109 (2003)","journal-title":"Information and Computation"},{"key":"3_CR21","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":"3_CR22","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":"3_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/BFb0013025","volume-title":"Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency","author":"A. Mazurkiewicz","year":"1989","unstructured":"Mazurkiewicz, A.: Basic notions of trace theory. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. LNCS, vol.\u00a0354, pp. 285\u2013363. Springer, Heidelberg (1989)"},{"key":"3_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1007\/3-540-44618-4_37","volume-title":"CONCUR 2000 - Concurrency Theory","author":"M. Mukund","year":"2000","unstructured":"Mukund, M., Narayan Kumar, K., Sohoni, M.: Synthesizing distributed finite-state systems from MSCs. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, pp. 521\u2013535. Springer, Heidelberg (2000)"},{"key":"3_CR25","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1991","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Heidelberg (1991)"},{"key":"3_CR26","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":"3_CR27","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":"3_CR28","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1142\/9789814261456_0006","volume-title":"The Book of Traces","author":"E. Ochmanski","year":"1995","unstructured":"Ochmanski, E.: Recognizable trace languages. In: Diekert, V., Rozenberg, G. (eds.) The Book of Traces, pp. 167\u2013204. World Scientific, Singapore (1995)"},{"key":"3_CR29","first-page":"139","volume-title":"FORTE\/PSTV 2000","author":"D. Peled","year":"2000","unstructured":"Peled, D.: Specification and verification of message sequence charts. In: FORTE\/PSTV 2000, pp. 139\u2013154. Kluwer, Pisa (2000)"},{"key":"3_CR30","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc.\u00a0of Logic in Computer Science (LICS 1986), pp. 332\u2013344 (1986)"}],"container-title":["Lecture Notes in Computer Science","Scenarios: Models, Transformations and Tools"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11495628_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T06:39:24Z","timestamp":1619505564000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11495628_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540261896","9783540320326"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/11495628_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}