{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,2]],"date-time":"2022-04-02T09:39:44Z","timestamp":1648892384236},"reference-count":46,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2017,7,24]],"date-time":"2017-07-24T00:00:00Z","timestamp":1500854400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2018,12]]},"DOI":"10.1007\/s10703-017-0282-y","type":"journal-article","created":{"date-parts":[[2017,7,24]],"date-time":"2017-07-24T13:51:40Z","timestamp":1500904300000},"page":"339-362","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Realizability of concurrent recursive programs"],"prefix":"10.1007","volume":"53","author":[{"given":"Benedikt","family":"Bollig","sequence":"first","affiliation":[]},{"given":"Manuela-Lidia","family":"Grindei","sequence":"additional","affiliation":[]},{"given":"Peter","family":"Habermehl","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,7,24]]},"reference":[{"key":"282_CR1","doi-asserted-by":"crossref","unstructured":"Atig MF, Bollig B, Habermehl P (2008) Emptiness of multi-pushdown automata is 2ETIME-complete. In: DLT\u201908, volume 5257 of LNCS. Springer, pp 121\u2013133","DOI":"10.1007\/978-3-540-85780-8_9"},{"key":"282_CR2","unstructured":"Akshay S, Dinca I, Genest B, Stefanescu A (2013) Implementing realistic asynchronous automata. In: FSTTCS\u201913, volume\u00a024 of Leibniz international proceedings in informatics. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, pp 213\u2013224"},{"key":"282_CR3","doi-asserted-by":"crossref","unstructured":"Aiswarya C, Gastin P, Narayan Kumar K (2014) Controllers for the verification of communicating multi-pushdown systems. In: CONCUR\u201914, volume 8704 of LNCS. Springer, pp 297\u2013311","DOI":"10.1007\/978-3-662-44584-6_21"},{"key":"282_CR4","doi-asserted-by":"crossref","unstructured":"Aiswarya C, Gastin P, Narayan Kumar K (2014) Verifying communicating multi-pushdown systems via split-width. In: ATVA\u201914, volume 8837 of LNCS. Springer, 1\u201317","DOI":"10.1007\/978-3-319-11936-6_1"},{"issue":"3","key":"282_CR5","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1516512.1516518","volume":"56","author":"R Alur","year":"2009","unstructured":"Alur R, Madhusudan P (2009) Adding nesting structure to words. J ACM 56(3):1\u201343","journal-title":"J ACM"},{"issue":"3","key":"282_CR6","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 (1996) Multi-push-down languages and grammars. Int J Found Comput Sci 7(3):253\u2013292","journal-title":"Int J Found Comput Sci"},{"issue":"4","key":"282_CR7","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 (2014) Temporal logics for concurrent recursive programs: satisfiability and model checking. J Appl Logic 12(4):395\u2013416","journal-title":"J Appl Logic"},{"key":"282_CR8","doi-asserted-by":"crossref","unstructured":"Bansal K, Demri S (2013) Model-checking bounded multi-pushdown systems. In: CSR\u201913, volume 7913 of LNCS. Springer, pp 405\u2013417","DOI":"10.1007\/978-3-642-38536-0_35"},{"key":"282_CR9","doi-asserted-by":"crossref","unstructured":"Bollig B, Grindei M-L, Habermehl P (2009) Realizability of concurrent recursive programs. In: FoSSaCS\u201909, volume 5504 of LNCS. Springer, pp 410\u2013424","DOI":"10.1007\/978-3-642-00596-1_29"},{"key":"282_CR10","doi-asserted-by":"crossref","unstructured":"Bollig B, Kuske D, Mennicke R (2013) The complexity of model checking multi-stack systems. In: LICS\u201913. IEEE Computer Society Press, pp 163\u2013170","DOI":"10.1109\/LICS.2013.22"},{"key":"282_CR11","doi-asserted-by":"crossref","unstructured":"Baudru N, Morin R (2007) Synthesis of safe message-passing systems. In: FSTTCS\u201907, volume 4855 of LNCS. Springer, 277\u2013289","DOI":"10.1007\/978-3-540-77050-3_23"},{"issue":"4:16","key":"282_CR12","first-page":"1","volume":"4","author":"B Bollig","year":"2008","unstructured":"Bollig B (2008) On the expressive power of 2-stack visibly pushdown automata. Log Methods Comput Sci 4(4:16):1\u201335","journal-title":"Log Methods Comput Sci"},{"key":"282_CR13","doi-asserted-by":"crossref","unstructured":"Cyriac A, Gastin P, Narayan Kumar K (2012) MSO decidability of multi-pushdown systems via split-width. In: Proceedings of CONCUR\u201912, volume 7454 of Lecture Notes in Computer Science. Springer, pp 547\u2013561","DOI":"10.1007\/978-3-642-32940-1_38"},{"key":"282_CR14","unstructured":"Cyriac A (2014) Verification of communicating recursive programs via split-width. Ph.D. thesis, Laboratoire Sp\u00e9cification et V\u00e9rification, ENS Cachan"},{"key":"282_CR15","volume-title":"The book of traces","year":"1995","unstructured":"Diekert V, Rozenberg G (eds) (1995) The book of traces. World Scientific, Singapore"},{"key":"282_CR16","doi-asserted-by":"crossref","unstructured":"Genest B, Gimbert H, Muscholl A, Walukiewicz I (2010) Optimal Zielonka-type construction of deterministic asynchronous automata. In: ICALP\u201910, volume 6199 of LNCS. Springer, pp 52\u201363","DOI":"10.1007\/978-3-642-14162-1_5"},{"issue":"6","key":"282_CR17","doi-asserted-by":"crossref","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 (2006) A Kleene theorem and model checking algorithms for existentially bounded communicating automata. Inf Comput 204(6):920\u2013956","journal-title":"Inf Comput"},{"issue":"1\u20133","key":"282_CR18","first-page":"147","volume":"80","author":"B Genest","year":"2007","unstructured":"Genest B, Kuske D, Muscholl A (2007) On communicating automata with bounded channels. Fundamenta Informaticae 80(1\u20133):147\u2013167","journal-title":"Fundamenta Informaticae"},{"key":"282_CR19","doi-asserted-by":"crossref","unstructured":"Genest B, Muscholl A (2006) Constructing exponential-size deterministic Zielonka automata. In: ICALP\u201906, volume 4052 of LNCS. Springer, pp 565\u2013576","DOI":"10.1007\/11787006_48"},{"issue":"3:23","key":"282_CR20","first-page":"1","volume":"8","author":"A Heu\u00dfner","year":"2012","unstructured":"Heu\u00dfner A, Leroux J, Muscholl A, Sutre G (2012) Reachability analysis of communicating pushdown systems. Log Methods Comput Sci 8(3:23):1\u201320","journal-title":"Log Methods Comput Sci"},{"issue":"1","key":"282_CR21","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.ic.2004.08.004","volume":"202","author":"JG Henriksen","year":"2005","unstructured":"Henriksen JG, Mukund M, Narayan Kumar K, Sohoni M, Thiagarajan PS (2005) A theory of regular MSC languages. Inf Comput 202(1):1\u201338","journal-title":"Inf Comput"},{"key":"282_CR22","doi-asserted-by":"crossref","first-page":"80","DOI":"10.1016\/S0890-5401(03)00123-8","volume":"187","author":"D Kuske","year":"2003","unstructured":"Kuske D (2003) Regular sets of infinite message sequence charts. Inf Comput 187:80\u2013109","journal-title":"Inf Comput"},{"issue":"1\u20133","key":"282_CR23","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1016\/j.tcs.2006.11.031","volume":"374","author":"D Kuske","year":"2007","unstructured":"Kuske D (2007) Weighted asynchronous cellular automata. Theor Comput Sci 374(1\u20133):127\u2013148","journal-title":"Theor Comput Sci"},{"issue":"2","key":"282_CR24","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1016\/j.ic.2003.10.002","volume":"189","author":"M Lohrey","year":"2004","unstructured":"Lohrey M, Muscholl A (2004) Bounded MSC communication. Inf Comput 189(2):160\u2013181","journal-title":"Inf Comput"},{"key":"282_CR25","doi-asserted-by":"crossref","unstructured":"La Torre S, Madhusudan P, Parlato G (2007) A robust class of context-sensitive languages. In: LICS\u201907. IEEE Computer Society Press, pp 161\u2013170","DOI":"10.1109\/LICS.2007.9"},{"key":"282_CR26","doi-asserted-by":"crossref","unstructured":"La Torre S, Madhusudan P, Parlato G (2008) Context-bounded analysis of concurrent queue systems. In: Proceedings of TACAS\u201908, volume 4963 of LNCS. Springer, pp 299\u2013314","DOI":"10.1007\/978-3-540-78800-3_21"},{"key":"282_CR27","doi-asserted-by":"crossref","unstructured":"La Torre S, Madhusudan P, Parlato G (2008) An infinite automaton characterization of double exponential time. In: CSL\u201908, volume 5213 of LNCS. Springer, 33\u201348","DOI":"10.1007\/978-3-540-87531-4_5"},{"key":"282_CR28","unstructured":"La Torre S, Napoli M (2011) Reachability of multistack pushdown systems with scope-bounded matching relations. In: CONCUR\u201911, volume 6901 of LNCS. Springer, pp 203\u2013218"},{"key":"282_CR29","doi-asserted-by":"crossref","unstructured":"La Torre S, Napoli M, Parlato G (2014) Scope-bounded pushdown languages. In DLT\u201914, volume 8633 of LNCS. Springer, pp 116\u2013128","DOI":"10.1007\/978-3-319-09698-8_11"},{"key":"282_CR30","doi-asserted-by":"crossref","unstructured":"La Torre S, Napoli M, Parlato G (2014) A unifying approach for multistack pushdown automata. In: MFCS\u201914, volume 8634 of LNCS, pages . Springer, 377\u2013389","DOI":"10.1007\/978-3-662-44522-8_32"},{"key":"282_CR31","unstructured":"La Torre S, Parlato G (2012) Scope-bounded multistack pushdown systems: fixed-point, sequentialization, and tree-width. In: FSTTCS\u201912, volume\u00a018 of Leibniz international proceedings in informatics. Leibniz-Zentrum f\u00fcr Informatik, pp 173\u2013184"},{"key":"282_CR32","doi-asserted-by":"crossref","unstructured":"Lal A, Touili T, Kidd N, Reps TW (2008) Interprocedural analysis of concurrent programs under a context bound. In: TACAS\u201908, volume 4963 of LNCS. Springer, pp 282\u2013298","DOI":"10.1007\/978-3-540-78800-3_20"},{"key":"282_CR33","doi-asserted-by":"crossref","unstructured":"Mazurkiewicz A (1977) Concurrent program schemes and their interpretations. DAIMI Rep. PB\u00a078, Aarhus University","DOI":"10.7146\/dpb.v6i78.7691"},{"key":"282_CR34","doi-asserted-by":"crossref","unstructured":"Mennicke R (2014) Model checking concurrent recursive programs using temporal logics. In: MFCS\u201914, volume 8634 of LNCS. Springer, pp 438\u2013450","DOI":"10.1007\/978-3-662-44522-8_37"},{"key":"282_CR35","doi-asserted-by":"crossref","unstructured":"Muscholl A, Peled D (1999) Message sequence graphs and decision problems on Mazurkiewicz traces. In: MFCS\u201999, volume 1672 of LNCS. Springer, pp 81\u201391","DOI":"10.1007\/3-540-48340-3_8"},{"key":"282_CR36","doi-asserted-by":"crossref","unstructured":"Madhusudan P, Parlato G (2011) The tree width of auxiliary storage. In: POPL\u201911. ACM, pp 283\u2013294","DOI":"10.1145\/1926385.1926419"},{"key":"282_CR37","unstructured":"Muscholl A (1994) \u00dcber die Erkennbarkeit unendlicher Spuren. Ph.D. thesis, Institut f\u00fcr Informatik, Universit\u00e4t Stuttgart"},{"key":"282_CR38","doi-asserted-by":"crossref","unstructured":"Ochma\u0144ski E (1995) Recognizable trace languages. In: Diekert V, Rozenberg G (eds) The book of traces, chapter\u00a06. World Scientific, Singapore, pp 167\u2013204","DOI":"10.1142\/9789814261456_0006"},{"key":"282_CR39","doi-asserted-by":"crossref","unstructured":"Otto F (2015) On visibly pushdown trace languages. In: SOFSEM\u201915, volume 8939 of Lecture Notes in Computer Science. Springer, pp 389\u2013400","DOI":"10.1007\/978-3-662-46078-8_32"},{"issue":"2","key":"282_CR40","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/S0304-3975(97)00219-3","volume":"195","author":"D Peled","year":"1998","unstructured":"Peled D, Wilke Th, Wolper P (1998) An algorithmic approach for checking closure properties of temporal logic specifications and omega-regular languages. Theor Comput Sci 195(2):183\u2013203","journal-title":"Theor Comput Sci"},{"key":"282_CR41","doi-asserted-by":"crossref","unstructured":"Qadeer S, Rehof J (2005) Context-bounded model checking of concurrent software. In: TACAS\u201905, volume 3440 of LNCS. Springer, 93\u2013107","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"282_CR42","unstructured":"Stefanescu A, Esparza J, Muscholl A (2003) Synthesis of distributed algorithms using asynchronous automata. In: CONCUR\u201903, volume 2761 of LNCS. Springer, pp 27\u201341"},{"key":"282_CR43","unstructured":"Stefanescu A (2006) Automatic synthesis of distributed transition systems. Ph.D. thesis, University of Stuttgart"},{"key":"282_CR44","unstructured":"Thomas W (1990) On logical definability of trace languages. In: Proceedings of algebraic and syntactic methods in computer science (ASMICS), Report TUM-I9002, Technical University of Munich, pp 172\u2013182"},{"key":"282_CR45","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/978-3-642-59126-6_7","volume-title":"Handbook of formal languages","author":"W Thomas","year":"1997","unstructured":"Thomas W (1997) Languages, automata and logic. In: Salomaa A, Rozenberg G (eds) Handbook of formal languages, vol 3. Springer, Berlin, pp 389\u2013455"},{"key":"282_CR46","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1051\/ita\/1987210200991","volume":"21","author":"W Zielonka","year":"1987","unstructured":"Zielonka W (1987) Notes on finite asynchronous automata. RAIRO Informatique Th\u00e9orique et Applications 21:99\u2013135","journal-title":"RAIRO Informatique Th\u00e9orique et Applications"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-017-0282-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0282-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0282-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,1]],"date-time":"2019-10-01T14:24:49Z","timestamp":1569939889000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-017-0282-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,7,24]]},"references-count":46,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2018,12]]}},"alternative-id":["282"],"URL":"https:\/\/doi.org\/10.1007\/s10703-017-0282-y","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,7,24]]}}}