{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:11:28Z","timestamp":1767928288587,"version":"3.49.0"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319119359","type":"print"},{"value":"9783319119366","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-11936-6_1","type":"book-chapter","created":{"date-parts":[[2014,10,24]],"date-time":"2014-10-24T15:11:50Z","timestamp":1414163510000},"page":"1-17","source":"Crossref","is-referenced-by-count":10,"title":["Verifying Communicating Multi-pushdown Systems via Split-Width"],"prefix":"10.1007","author":[{"given":"C.","family":"Aiswarya","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paul","family":"Gastin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"K.","family":"Narayan Kumar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"1_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1516512.1516518","volume":"56","author":"R. Alur","year":"2009","unstructured":"Alur, R., Madhusudan, P.: Adding nesting structure to words. Journal of the ACM\u00a056(3), 1\u201343 (2009)","journal-title":"Journal of the ACM"},{"key":"1_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-540-85780-8_9","volume-title":"Developments in Language Theory","author":"M.F. Atig","year":"2008","unstructured":"Atig, M.F., Bollig, B., Habermehl, P.: Emptiness of multi-pushdown automata is 2ETIME-Complete. In: Ito, M., Toyama, M. (eds.) DLT 2008. LNCS, vol.\u00a05257, pp. 121\u2013133. Springer, Heidelberg (2008)"},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-642-22993-0_15","volume-title":"Mathematical Foundations of Computer Science 2011","author":"B. Bollig","year":"2011","unstructured":"Bollig, B., Cyriac, A., Gastin, P., Zeitoun, M.: Temporal logics for concurrent recursive programs: Satisfiability and model checking. In: Murlak, F., Sankowski, P. (eds.) MFCS 2011. LNCS, vol.\u00a06907, pp. 132\u2013144. Springer, Heidelberg (2011)"},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"Bollig, B., Kuske, D., Meinecke, I.: Propositional dynamic logic for message-passing systems. Logical Methods in Computer Science\u00a06(3:16) (2010)","DOI":"10.2168\/LMCS-6(3:16)2010"},{"issue":"3","key":"1_CR5","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1142\/S0129054196000191","volume":"7","author":"L. Breveglieri","year":"1996","unstructured":"Breveglieri, L., Cherubini, A., Citrini, C., Crespi-Reghizzi, S.: Multi-pushdown languages and grammars. Int. J. Found. Comput. Sci.\u00a07(3), 253\u2013292 (1996)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"1_CR6","unstructured":"Courcelle, B.: Special tree-width and the verification of monadic second-order graph properties. In: FSTTCS. LIPIcs, vol.\u00a08, pp. 13\u201329 (2010)"},{"key":"1_CR7","unstructured":"Cyriac, A.: Verification of Communicating Recursive Programs via Split-width. PhD thesis, ENS Cachan (2014), \n                  \n                    http:\/\/www.lsv.ens-cachan.fr\/~cyriac\/download\/Thesis_Aiswarya_Cyriac.pdf"},{"key":"1_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1007\/978-3-642-32940-1_38","volume-title":"CONCUR 2012 \u2013 Concurrency Theory","author":"A. Cyriac","year":"2012","unstructured":"Cyriac, A., Gastin, P., Narayan Kumar, K.: MSO decidability of multi-pushdown systems via split-width. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol.\u00a07454, pp. 547\u2013561. Springer, Heidelberg (2012)"},{"key":"1_CR9","unstructured":"Cyriac, A., Gastin, P., Narayan Kumar, K.: Verifying Communicating Multi-pushdown Systems. Technical report (January 2014), \n                  \n                    http:\/\/hal.archives-ouvertes.fr\/hal-00943690"},{"issue":"2","key":"1_CR10","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/s10703-011-0136-y","volume":"40","author":"P. Ganty","year":"2012","unstructured":"Ganty, P., Majumdar, R., Monmege, B.: Bounded underapproximations. Formal Methods in System Design\u00a040(2), 206\u2013231 (2012)","journal-title":"Formal Methods in System Design"},{"issue":"6","key":"1_CR11","doi-asserted-by":"publisher","first-page":"920","DOI":"10.1016\/j.ic.2006.01.005","volume":"204","author":"B. Genest","year":"2006","unstructured":"Genest, B., Kuske, D., Muscholl, A.: A Kleene theorem and model checking algorithms for existentially bounded communicating automata. Inf. Comput.\u00a0204(6), 920\u2013956 (2006)","journal-title":"Inf. Comput."},{"issue":"1","key":"1_CR12","doi-asserted-by":"publisher","first-page":"279","DOI":"10.2178\/jsl\/1231082313","volume":"74","author":"S. G\u00f6ller","year":"2009","unstructured":"G\u00f6ller, S., Lohrey, M., Lutz, C.: PDL with intersection and converse: satisfiability and infinite-state model checking. J. Symb. Log.\u00a074(1), 279\u2013314 (2009)","journal-title":"J. Symb. Log."},{"issue":"1","key":"1_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.ic.2004.08.004","volume":"202","author":"J.G. Henriksen","year":"2005","unstructured":"Henriksen, J.G., Mukund, M., Narayan Kumar, K., Sohoni, M.A., Thiagarajan, P.S.: A theory of regular MSC languages. Inf. Comput.\u00a0202(1), 1\u201338 (2005)","journal-title":"Inf. Comput."},{"issue":"1-3","key":"1_CR14","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1016\/S0168-0072(98)00039-6","volume":"96","author":"J.G. Henriksen","year":"1999","unstructured":"Henriksen, J.G., Thiagarajan, P.S.: Dynamic linear time temporal logic. Ann. Pure Appl. Logic\u00a096(1-3), 187\u2013207 (1999)","journal-title":"Ann. Pure Appl. Logic"},{"key":"1_CR15","unstructured":"Heu\u00dfner, A.: Model checking communicating processes: Run graphs, graph grammars, and MSO. ECEASST\u00a047 (2012)"},{"key":"1_CR16","unstructured":"ITU-TS. ITU-TS Recommendation Z.120: Message Sequence Chart (MSC). ITU-TS, Geneva (February 2011)"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: A robust class of context-sensitive languages. In: LICS, pp. 161\u2013170. IEEE Computer Society (2007)","DOI":"10.1109\/LICS.2007.9"},{"key":"1_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-540-87531-4_5","volume-title":"Computer Science Logic","author":"S. Torre La","year":"2008","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: An infinite automaton characterization of double exponential time. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol.\u00a05213, pp. 33\u201348. Springer, Heidelberg (2008)"},{"key":"1_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/978-3-642-23217-6_14","volume-title":"CONCUR 2011 \u2013 Concurrency Theory","author":"S. Torre La","year":"2011","unstructured":"La Torre, S., Napoli, M.: Reachability of multistack pushdown systems with scope-bounded matching relations. In: Katoen, J.-P., K\u00f6nig, B. (eds.) CONCUR 2011. LNCS, vol.\u00a06901, pp. 203\u2013218. Springer, Heidelberg (2011)"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Madhusudan, P., Parlato, G.: The tree width of auxiliary storage. In: Ball, T., Sagiv, M. (eds.) POPL, pp. 283\u2013294. ACM (2011)","DOI":"10.1145\/1925844.1926419"},{"key":"1_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-540-31980-1_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Qadeer","year":"2005","unstructured":"Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 93\u2013107. Springer, Heidelberg (2005)"},{"key":"1_CR22","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/3-540-15648-8_31","volume-title":"Logics of Programs","author":"M.Y. Vardi","year":"1985","unstructured":"Vardi, M.Y.: The taming of converse: Reasoning about two-way computations. In: Parikh, R. (ed.) Logics of Programs. LNCS, vol.\u00a0193, pp. 413\u2013423. Springer, Heidelberg (1985)"},{"key":"1_CR23","first-page":"99","volume":"21","author":"W. Zielonka","year":"1987","unstructured":"Zielonka, W.: Notes on finite asynchronous automata. R.A.I.R.O. \u2014 Informatique Th\u00e9orique et Applications\u00a021, 99\u2013135 (1987)","journal-title":"R.A.I.R.O. \u2014 Informatique Th\u00e9orique et Applications"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-11936-6_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,28]],"date-time":"2019-05-28T03:20:24Z","timestamp":1559013624000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-11936-6_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319119359","9783319119366"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-11936-6_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}