{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,26]],"date-time":"2024-07-26T09:58:46Z","timestamp":1721987926140},"reference-count":29,"publisher":"Elsevier BV","issue":"6","license":[{"start":{"date-parts":[[2006,6,1]],"date-time":"2006-06-01T00:00:00Z","timestamp":1149120000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":2603,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Information and Computation"],"published-print":{"date-parts":[[2006,6]]},"DOI":"10.1016\/j.ic.2006.01.005","type":"journal-article","created":{"date-parts":[[2006,5,5]],"date-time":"2006-05-05T06:20:11Z","timestamp":1146810011000},"page":"920-956","source":"Crossref","is-referenced-by-count":40,"title":["A Kleene theorem and model checking algorithms for existentially bounded communicating automata"],"prefix":"10.1016","volume":"204","author":[{"given":"Blaise","family":"Genest","sequence":"first","affiliation":[]},{"given":"Dietrich","family":"Kuske","sequence":"additional","affiliation":[]},{"given":"Anca","family":"Muscholl","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"issue":"2","key":"10.1016\/j.ic.2006.01.005_bib1","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1006\/inco.1996.0053","article-title":"Verifying programs with unreliable channels","volume":"12","author":"Abdulla","year":"1996","journal-title":"Inf. Comput."},{"key":"10.1016\/j.ic.2006.01.005_bib2","unstructured":"R. Alur, M. Yannakakis. Model checking of message sequence charts, in: CONCUR\u201999, Lecture Notes in Computer Science, vol. 1664, 1999, pp. 114\u2013129."},{"key":"10.1016\/j.ic.2006.01.005_bib3","series-title":"Transductions and context-free languages","author":"Berstel","year":"1979"},{"issue":"1\u20132","key":"10.1016\/j.ic.2006.01.005_bib4","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1016\/S0304-3975(99)00033-X","article-title":"Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations","volume":"22","author":"Bouajjani","year":"1999","journal-title":"Theor. Comput. Sci."},{"key":"10.1016\/j.ic.2006.01.005_bib5","unstructured":"B. Boigelot, P. Godefroid, B. Willems, P. Wolper, The Power of QDDs, in: SAS\u201997, Lecture Notes in Computer Science, vol. 1302, 1997, pp. 172\u2013186."},{"issue":"3","key":"10.1016\/j.ic.2006.01.005_bib6","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1023\/A:1008719024240","article-title":"Symbolic verification of communication protocols with infinite state spaces using QDDs","volume":"1","author":"Boigelot","year":"1999","journal-title":"Formal Methods Syst. Des."},{"key":"10.1016\/j.ic.2006.01.005_bib7","doi-asserted-by":"crossref","unstructured":"B. Bollig, M. Leucker, Message-passing automata are expressively equivalent to EMSO Logic, Theor. Comput. Sci. 2006 (in press). (An extended abstract appeared under the same title in CONCUR\u201904, Lecture Notes in Computer Science, vol. 3170, 2004, pp. 146\u2013160).","DOI":"10.1007\/978-3-540-28644-8_10"},{"issue":"2","key":"10.1016\/j.ic.2006.01.005_bib8","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1145\/322374.322380","article-title":"On communicating finite-state machines","volume":"3","author":"Brand","year":"1983","journal-title":"J. ACM"},{"key":"10.1016\/j.ic.2006.01.005_bib9","series-title":"The Book of Traces","year":"1995"},{"key":"10.1016\/j.ic.2006.01.005_bib10","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1016\/0304-3975(95)00130-1","article-title":"Logical definability on infinite traces","volume":"154","author":"Ebinger","year":"1996","journal-title":"Theor. Comput. Sci."},{"issue":"1,2","key":"10.1016\/j.ic.2006.01.005_bib11","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1016\/S0304-3975(00)00102-X","article-title":"Well-structured transition systems everywhere!","volume":"256","author":"Finkel","year":"2001","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"10.1016\/j.ic.2006.01.005_bib12","doi-asserted-by":"crossref","first-page":"78","DOI":"10.1007\/s10009-002-0085-2","article-title":"Compositional message sequence charts","author":"Gunter","year":"2003","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"key":"10.1016\/j.ic.2006.01.005_bib13","doi-asserted-by":"crossref","unstructured":"B. Genest, A. Muscholl, H. Seidl, M. Zeitoun, Infinite-state High-level MSCs: model checking and realizability, in: ICALP\u201902, Lecture Notes in Computer Science, vol. 2380, 2002, pp. 657\u2013668. Journal version in Journal of Computer and System Sciences (2006), in press.","DOI":"10.1007\/3-540-45465-9_56"},{"issue":"1","key":"10.1016\/j.ic.2006.01.005_bib14","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.ic.2004.08.004","article-title":"A theory of regular MSC languages","volume":"20","author":"Henriksen","year":"2005","journal-title":"Inf. Comput."},{"key":"10.1016\/j.ic.2006.01.005_bib15","unstructured":"ITU-TS recommendation Z.120, Message Sequence Charts, Geneva, 1999."},{"key":"10.1016\/j.ic.2006.01.005_bib16","doi-asserted-by":"crossref","first-page":"80","DOI":"10.1016\/S0890-5401(03)00123-8","article-title":"Regular sets of infinite message sequence charts","volume":"187","author":"Kuske","year":"2003","journal-title":"Inf. Comput."},{"key":"10.1016\/j.ic.2006.01.005_bib17","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/j.ic.2003.10.002","article-title":"Bounded MSC communication","volume":"189","author":"Lohrey","year":"2004","journal-title":"Inf. Comput."},{"key":"10.1016\/j.ic.2006.01.005_bib18","unstructured":"S. Leue, R. Mayr, W. Wei, A scalable incomplete test for the boundedness of UML RT models, in: TACAS\u201904, Lecture Notes in Computer Science, vol. 2988, 2004, pp. 327\u2013341."},{"key":"10.1016\/j.ic.2006.01.005_bib19","series-title":"Proc. Logic Colloquium","first-page":"132","article-title":"Weak monadic second order theory of one successor is not elementary recursive","volume":"vol. 453","author":"Meyer","year":"1975"},{"key":"10.1016\/j.ic.2006.01.005_bib20","unstructured":"R. Morin, Recognizable sets of message sequence charts, in: STACS\u201902, Lecture Notes in Computer Science, vol. 2285, 2002, pp. 523\u2013534."},{"key":"10.1016\/j.ic.2006.01.005_bib21","unstructured":"P. Madhusudan, Reasoning about sequential and branching behaviours of message sequence graphs, in: ICALP\u201901, Lecture Notes in Computer Science, vol. 2076, 2001, pp. 809\u2013820."},{"key":"10.1016\/j.ic.2006.01.005_bib22","unstructured":"P. Madhusudan, B. Meenakshi, Beyond message sequence graphs, in: FSTTCS\u201901, Lecture Notes in Computer Science, vol. 2245, 2001, pp. 256\u2013267."},{"key":"10.1016\/j.ic.2006.01.005_bib23","doi-asserted-by":"crossref","unstructured":"A. Mazurkiewicz, Concurrent program schemes and their interpretation, Technical report, DAIMI Report PB-78, Aarhus University, 1977.","DOI":"10.7146\/dpb.v6i78.7691"},{"key":"10.1016\/j.ic.2006.01.005_bib24","unstructured":"A. Muscholl, D. Peled, Message sequence graphs and decision problems on Mazurkiewicz traces, in: MFCS\u201999, Lecture Notes in Computer Science, vol. 1672, 1999, pp. 81\u201391."},{"key":"10.1016\/j.ic.2006.01.005_bib25","unstructured":"E. Ochma\u0144ski, Regular behaviour of concurrent systems, in: Bulletin of the EATCS 27, 1985, pp. 56\u201367."},{"issue":"5","key":"10.1016\/j.ic.2006.01.005_bib26","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1016\/S0020-0190(01)00337-4","article-title":"Verifying lossy channel systems has nonprimitive recursive complexity","volume":"8","author":"Schnoebelen","year":"2002","journal-title":"Inf. Process. Lett."},{"key":"10.1016\/j.ic.2006.01.005_bib27","unstructured":"USB 1.1 specification. ."},{"key":"10.1016\/j.ic.2006.01.005_bib28","unstructured":"W. Thomas, On logical definability of trace languages, in: V. Diekert (Ed.), Proceedings of a workshop of the ESPRIT BRA No. 3166: Algebraic and Syntactic Methods in Computer Science (ASMICS) 1989, Report TUM-I9002, Technical University of Munich, 1990, pp. 172\u2013182."},{"key":"10.1016\/j.ic.2006.01.005_bib29","first-page":"99","article-title":"Notes on finite asynchronous automata","volume":"21","author":"Zielonka","year":"1987","journal-title":"R.A.I.R.O.\u2014Inf. Th\u00e9or. Appl."}],"container-title":["Information and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0890540106000290?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0890540106000290?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,18]],"date-time":"2019-04-18T16:26:27Z","timestamp":1555604787000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0890540106000290"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,6]]},"references-count":29,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2006,6]]}},"alternative-id":["S0890540106000290"],"URL":"https:\/\/doi.org\/10.1016\/j.ic.2006.01.005","relation":{},"ISSN":["0890-5401"],"issn-type":[{"value":"0890-5401","type":"print"}],"subject":[],"published":{"date-parts":[[2006,6]]}}}