{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,10]],"date-time":"2025-06-10T14:40:02Z","timestamp":1749566402457,"version":"3.41.0"},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2016,8,26]],"date-time":"2016-08-26T00:00:00Z","timestamp":1472169600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Theory Comput Syst"],"published-print":{"date-parts":[[2017,5]]},"DOI":"10.1007\/s00224-016-9700-6","type":"journal-article","created":{"date-parts":[[2016,8,26]],"date-time":"2016-08-26T02:39:42Z","timestamp":1472179182000},"page":"695-736","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["The Complexity of Model Checking Multi-Stack Systems"],"prefix":"10.1007","volume":"60","author":[{"given":"Benedikt","family":"Bollig","sequence":"first","affiliation":[]},{"given":"Dietrich","family":"Kuske","sequence":"additional","affiliation":[]},{"given":"Roy","family":"Mennicke","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,8,26]]},"reference":[{"key":"9700_CR1","doi-asserted-by":"crossref","unstructured":"Aiswarya, C., Gastin, P., Narayan Kumar, K.: Verifying communicating multi-pushdown systems via split-width. In: Proceedings of ATVA\u201914, pp 1\u201317 (2014)","DOI":"10.1007\/978-3-319-11936-6_1"},{"issue":"11","key":"9700_CR2","first-page":"1","volume":"4","author":"R Alur","year":"2008","unstructured":"Alur, R., Arenas, M., Barcel\u00f3, P., Etessami, K., Immerman, N., Libkin, L.: First-order and temporal logics for nested words. Logical Methods Comput Sci 4(11), 1\u201344 (2008)","journal-title":"Logical Methods Comput Sci"},{"key":"9700_CR3","doi-asserted-by":"crossref","unstructured":"Alur, R., Etessami, K., Madhusudan, P.: A Temporal Logic of Nested Calls and Returns. In: Proceedings of TACAS\u201904, vol. 2988 of Lecture Notes in Computer Science, pp 467\u2013481. Springer (2004)","DOI":"10.1007\/978-3-540-24730-2_35"},{"key":"9700_CR4","doi-asserted-by":"crossref","first-page":"16:1","DOI":"10.1145\/1516512.1516518","volume":"56","author":"R Alur","year":"2009","unstructured":"Alur, R., Madhusudan, P.: Adding nesting structure to words. J ACM 56, 16:1\u201316:43 (2009)","journal-title":"J ACM"},{"key":"9700_CR5","first-page":"3","volume":"8","author":"MF Atig","year":"2012","unstructured":"Atig, M.F.: Model-checking of ordered multi-pushdown automata. Logical Methods Comput Sci 8, 3 (2012)","journal-title":"Logical Methods Comput Sci"},{"key":"9700_CR6","doi-asserted-by":"crossref","unstructured":"Atig, M.F., Bollig, B., Habermehl, P.: Emptiness of multi-pushdown automata is 2ETIME-complete. In: Proceedings of DLT\u201908, vol. 5257 of Lecture Notes in Computer Science, pp 121\u2013133. Springer (2008)","DOI":"10.1007\/978-3-540-85780-8_9"},{"key":"9700_CR7","doi-asserted-by":"crossref","unstructured":"Atig, M.F., Bouajjani, A., Narayan Kumar, K., Saivasan, P.: Linear-time model-checking for multithreaded programs under scope-bounding. In: Proceedings of ATVA\u201912, vol. 7561, pp 152\u2013166. Springer (2012)","DOI":"10.1007\/978-3-642-33386-6_13"},{"key":"9700_CR8","unstructured":"Atig, M.F., Bouajjani, A., Narayan Kumar, K., Saivasan, P.: Model checking branching-time properties of multi-pushdown systems is hard (2012). CoRR, arXiv: 1205.6928"},{"key":"9700_CR9","unstructured":"Baier, C., Katoen, J.-P.: Principles of model checking. MIT Press (2008)"},{"issue":"4","key":"9700_CR10","doi-asserted-by":"crossref","first-page":"395","DOI":"10.1016\/j.jal.2014.05.001","volume":"12","author":"B Bollig","year":"2014","unstructured":"Bollig, B., Cyriac, A., Gastin, P., Zeitoun, M.: Temporal logics for concurrent recursive programs: satisfiability and model checking. J. Applied Logic 12(4), 395\u2013416 (2014)","journal-title":"J. Applied Logic"},{"issue":"2","key":"9700_CR11","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1016\/j.jal.2012.01.002","volume":"10","author":"B Bollig","year":"2012","unstructured":"Bollig, B., Kuske, D.: An optimal construction of Hanf sentences. J. Appl. Log. 10(2), 179\u2013186 (2012)","journal-title":"J. Appl. Log."},{"key":"9700_CR12","doi-asserted-by":"crossref","unstructured":"Bollig, B., Kuske, D., Mennicke, R.: The complexity of model checking multi-stack systems. In: Proceedings of LICS\u201913, pp 163\u2013172. IEEE Computer Society (2013)","DOI":"10.1109\/LICS.2013.22"},{"issue":"3","key":"9700_CR13","doi-asserted-by":"crossref","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-push-down languages and grammars. Int. J. Found. Comput. Sci. 7(3), 253\u2013292 (1996)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"9700_CR14","doi-asserted-by":"crossref","unstructured":"Clarke, E. M., Grumberg, O., Peled, D.: Model checking. MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50026-6"},{"key":"9700_CR15","doi-asserted-by":"crossref","unstructured":"Cyriac, A., Gastin, P., Narayan Kumar, K.: MSO decidability of multi-pushdown systems via split-width. In: Proceedings of CONCUR\u201912, volume 7454 of Lecture Notes in Computer Science, pp 547\u2013561. Springer (2012)","DOI":"10.1007\/978-3-642-32940-1_38"},{"key":"9700_CR16","doi-asserted-by":"crossref","unstructured":"Ebbinghaus, H.-D., Flum, J.: Finite model theory. Springer (1995)","DOI":"10.1007\/3-540-28788-4"},{"key":"9700_CR17","doi-asserted-by":"crossref","unstructured":"Fagin, R., Stockmeyer, L.J., Vardi, M.: On monadic NP vs. monadic co-NP (Extended Abstract). In: Structure in complexity theory conference, pp 19\u201330. IEEE Computer Society Press (1993)","DOI":"10.1109\/SCT.1993.336544"},{"key":"9700_CR18","doi-asserted-by":"crossref","unstructured":"Gabbay, D.M., Hodkinson, I., Reynolds, M.A.: Temporal logic: Mathematical foundations and computational aspects, vol. 1. Oxford University Press (1994)","DOI":"10.1007\/BFb0013976"},{"key":"9700_CR19","doi-asserted-by":"crossref","unstructured":"Gastin, P., Kuske, D.: Uniform satisfiability problem for local temporal logics over Mazurkiewicz traces. In: Proceedings of CONCUR\u201905 Lecture Notes in Comp. Science, vol. 3653, pp 533\u2013547. Springer (2005)","DOI":"10.1007\/11539452_40"},{"issue":"7","key":"9700_CR20","doi-asserted-by":"crossref","first-page":"797","DOI":"10.1016\/j.ic.2009.12.003","volume":"208","author":"P Gastin","year":"2010","unstructured":"Gastin, P., Kuske, D.: Uniform satisfiability problem for local temporal logics over Mazurkiewicz traces. Inf. Comput. 208(7), 797\u2013816 (2010)","journal-title":"Inf. Comput."},{"key":"9700_CR21","unstructured":"G\u00f6ller, S., Lin, A.W.: Concurrency makes simple theories hard. In: Proceedings of STACS\u201912, Volume 14 of Leibniz International Proceedings in Informatics (LIPIcs), pp 148\u2013159 (2012)"},{"key":"9700_CR22","doi-asserted-by":"crossref","unstructured":"Hanf, W.: Model-theoretic methods in the study of elementary logic. In: The theory of models, pp 132\u2013145. North Holland (1965)","DOI":"10.1016\/B978-0-7204-2233-7.50020-4"},{"issue":"3:23","key":"9700_CR23","first-page":"1","volume":"8","author":"A Heu\u00dfner","year":"2012","unstructured":"Heu\u00dfner, A., Leroux, J., Muscholl, A., Sutre, G.: Reachability analysis of communicating pushdown systems. Logical Methods Comput Sci 8(3:23), 1\u201320 (2012)","journal-title":"Logical Methods Comput Sci"},{"key":"9700_CR24","doi-asserted-by":"crossref","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: A robust class of context-sensitive languages. In: Proceedings of LICS\u201907, pp 161\u2013170. IEEE Computer Society Press (2007)","DOI":"10.1109\/LICS.2007.9"},{"key":"9700_CR25","doi-asserted-by":"crossref","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: Context-bounded analysis of concurrent queue systems. In: Proceedings of TACAS\u201908 Lecture Notes in Computer Science, pp 299\u2013314. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_21"},{"key":"9700_CR26","doi-asserted-by":"crossref","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: An infinite automaton characterization of double exponential time. In: Proceedings of CSL\u201908, volume 5213 of Lecture Notes in Computer Science. Springer (2008)","DOI":"10.1007\/978-3-540-87531-4_5"},{"key":"9700_CR27","doi-asserted-by":"crossref","unstructured":"La Torre, S., Napoli, M.: Reachability of multistack pushdown systems with scope-bounded matching relations. In: Proceedings of CONCUR 2011, volume 6901 of Lecture Notes in Computer Science, pp 203\u2013218. Springer (2011)","DOI":"10.1007\/978-3-642-23217-6_14"},{"key":"9700_CR28","doi-asserted-by":"crossref","unstructured":"La Torre, S., Napoli, M.: A temporal logic for multi-threaded programs. In: Proceedings of IFIP-TCS\u201912, Volume 7604 of Lecture Notes in Computer Science, pp 225\u2013239. Springer (2012)","DOI":"10.1007\/978-3-642-33475-7_16"},{"key":"9700_CR29","unstructured":"La Torre, S., Parlato, G.: Scope-bounded multistack pushdown systems: Fixed-point, sequentialization, and tree-width. In: Proceedings of FSTTCS\u201912, Volume 18 of Leibniz International Proceedings in Informatics (LIPIcs), pp 173\u2013184 (2012)"},{"key":"9700_CR30","doi-asserted-by":"crossref","unstructured":"Madhusudan, P., Parlato, G.: The tree width of auxiliary storage. In: Proceedings of POPL\u201911, pp 283\u2013294. ACM (2011)","DOI":"10.1145\/1926385.1926419"},{"key":"9700_CR31","doi-asserted-by":"crossref","unstructured":"Matz, O., Thomas, W.: The monadic quantifier alternation hierarchy over graphs is infinite. In: LICS\u201997, pp 236\u2013244. IEEE Computer Society Press (1997)","DOI":"10.1109\/LICS.1997.614951"},{"key":"9700_CR32","doi-asserted-by":"crossref","unstructured":"Mennicke, R.: Model checking concurrent recursive programs using temporal logics. In: Proceedings of MFCS\u201914, Part I, volume 8634 of Lecture Notes in Computer Science, pp 438\u2013450. Springer (2014)","DOI":"10.1007\/978-3-662-44522-8_37"},{"key":"9700_CR33","unstructured":"Mennicke, R.: Model checking concurrent systems using temporal logics. PhD Thesis, Fakult\u00e4t f\u00fcr Informatik und Automatisierung, Technische Universit\u00e4t Ilmenau (2015)"},{"key":"9700_CR34","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of FOCS\u201977, pp 46\u201357. IEEE (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"9700_CR35","doi-asserted-by":"crossref","unstructured":"Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Proceedings of TACAS\u201905, Volume 3440 of Lecture Notes in Computer Science, pp 93\u2013107. Springer (2005)","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"9700_CR36","doi-asserted-by":"crossref","unstructured":"Reinhardt, K.: The complexity of translating logic to finite automata. In: Automata, logics, and infinite games, volume 2500 of Lecture Notes in Computer Science, pp 231\u2013238. Springer (2002)","DOI":"10.1007\/3-540-36387-4_13"},{"key":"9700_CR37","unstructured":"Stockmeyer, L.: The complexity of decision problems in automata theory and logic. PhD thesis, MIT (1974)"}],"container-title":["Theory of Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-016-9700-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00224-016-9700-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-016-9700-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-016-9700-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,10]],"date-time":"2025-06-10T14:24:01Z","timestamp":1749565441000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00224-016-9700-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,8,26]]},"references-count":37,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2017,5]]}},"alternative-id":["9700"],"URL":"https:\/\/doi.org\/10.1007\/s00224-016-9700-6","relation":{},"ISSN":["1432-4350","1433-0490"],"issn-type":[{"type":"print","value":"1432-4350"},{"type":"electronic","value":"1433-0490"}],"subject":[],"published":{"date-parts":[[2016,8,26]]}}}