{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T08:00:41Z","timestamp":1743062441772,"version":"3.40.3"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030720155"},{"type":"electronic","value":"9783030720162"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,20]],"date-time":"2021-03-20T00:00:00Z","timestamp":1616198400000},"content-version":"vor","delay-in-days":78,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The model of asynchronous programming arises in many contexts, from low-level systems software to high-level web programming. We take a language-theoretic perspective and show general decidability and undecidability results for asynchronous programs that capture all known results as well as show decidability of new and important classes. As a main consequence, we show decidability of safety, termination and boundedness verification for <jats:italic>higher-order<\/jats:italic> asynchronous programs\u2014such as OCaml programs using Lwt\u2014and undecidability of liveness verification already for order-2 asynchronous programs. We show that under mild assumptions, surprisingly, safety and termination verification of asynchronous programs with handlers from a language class are decidable <jats:italic>iff<\/jats:italic> emptiness is decidable for the underlying language class. Moreover, we show that configuration reachability and liveness (fair termination) verification are equivalent, and decidability of these problems implies decidability of the well-known \u201cequal-letters\u201d problem on languages. Our results close the decidability frontier for asynchronous programs.<\/jats:p>","DOI":"10.1007\/978-3-030-72016-2_24","type":"book-chapter","created":{"date-parts":[[2021,3,19]],"date-time":"2021-03-19T22:03:37Z","timestamp":1616191417000},"page":"449-467","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["General Decidability Results for Asynchronous Shared-Memory Programs: Higher-Order and Beyond"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2136-0542","authenticated-orcid":false,"given":"Rupak","family":"Majumdar","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9926-0931","authenticated-orcid":false,"given":"Ramanathan S.","family":"Thinniyam","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6421-4388","authenticated-orcid":false,"given":"Georg","family":"Zetzsche","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,3,20]]},"reference":[{"key":"24_CR1","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Bouajjani, A., Jonsson, B.: On-the-fly analysis of systems with unbounded, lossy FIFO channels. In: Proceedings of the 10th International Conference on Computer Aided Verification (CAV 1998). pp. 305\u2013318 (1998). https:\/\/doi.org\/10.1007\/BFb0028754","DOI":"10.1007\/BFb0028754"},{"key":"24_CR2","doi-asserted-by":"publisher","unstructured":"Aho, A.V.: Indexed grammars - an extension of context-free grammars. J. ACM 15(4), 647\u2013671 (1968). https:\/\/doi.org\/10.1145\/321479.321488","DOI":"10.1145\/321479.321488"},{"key":"24_CR3","doi-asserted-by":"crossref","unstructured":"Atig, M.F., Bouajjani, A., Qadeer, S.: Context-bounded analysis for concurrent programs with dynamic creation of threads. In: Proceedings of TACAS 2009. pp. 107\u2013123 (2009)","DOI":"10.1007\/978-3-642-00768-2_11"},{"key":"24_CR4","doi-asserted-by":"crossref","unstructured":"Bachmeier, G., Luttenberger, M., Schlund, M.: Finite automata for the sub- and superword closure of CFLs: Descriptional and computational complexity. In: Proceedings of LATA 2015. pp. 473\u2013485 (2015)","DOI":"10.1007\/978-3-319-15579-1_37"},{"key":"24_CR5","doi-asserted-by":"crossref","unstructured":"Berstel, J.: Transductions and context-free languages. Teubner-Verlag (1979)","DOI":"10.1007\/978-3-663-09367-1"},{"key":"24_CR6","doi-asserted-by":"crossref","unstructured":"Chadha, R., Viswanathan, M.: Decidability results for well-structured transition systems with auxiliary storage. In: CONCUR \u201907: Proc. 18th Int. Conf. on Concurrency Theory. LNCS, vol. 4703, pp. 136\u2013150. Springer (2007)","DOI":"10.1007\/978-3-540-74407-8_10"},{"key":"24_CR7","doi-asserted-by":"publisher","unstructured":"Clemente, L., Parys, P., Salvati, S., Walukiewicz, I.: The diagonal problem for higher-order recursion schemes is decidable. In: Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS \u201916, New York, NY, USA, July 5\u20138, 2016. pp. 96\u2013105. ACM (2016). https:\/\/doi.org\/10.1145\/2933575.2934527","DOI":"10.1145\/2933575.2934527"},{"key":"24_CR8","unstructured":"Courcelle, B.: On constructing obstruction sets of words. Bulletin of the EATCS 44, 178\u2013186 (1991)"},{"key":"24_CR9","doi-asserted-by":"crossref","unstructured":"Damm, W.: The IO-and OI-hierarchies. Theoretical Computer Science 20(2), 95\u2013207 (1982)","DOI":"10.1016\/0304-3975(82)90009-3"},{"key":"24_CR10","doi-asserted-by":"crossref","unstructured":"Damm, W., Goerdt, A.: An automata-theoretical characterization of the OI-hierarchy. Information and Control 71(1), 1\u201332 (1986)","DOI":"10.1016\/S0019-9958(86)80016-X"},{"key":"24_CR11","doi-asserted-by":"crossref","unstructured":"Dufourd, C., Finkel, A., Schnoebelen, P.: Reset nets between decidability and undecidability. In: Proceedings of ICALP 1998. pp. 103\u2013115 (1998)","DOI":"10.1007\/BFb0055044"},{"key":"24_CR12","doi-asserted-by":"crossref","unstructured":"Ganty, P., Majumdar, R.: Algorithmic verification of asynchronous programs. ACM Transactions on Programming Languages and Systems (TOPLAS) 34(1), 6 (2012)","DOI":"10.1145\/2160910.2160915"},{"key":"24_CR13","doi-asserted-by":"publisher","unstructured":"Geeraerts, G., Raskin, J., Begin, L.V.: Well-structured languages. Acta Inf. 44(3\u20134), 249\u2013288 (2007). https:\/\/doi.org\/10.1007\/s00236-007-0050-3","DOI":"10.1007\/s00236-007-0050-3"},{"key":"24_CR14","doi-asserted-by":"publisher","unstructured":"Greibach, S.A.: Remarks on blind and partially blind one-way multicounter machines. Theoretical Computer Science 7(3), 311 \u2013 324 (1978). https:\/\/doi.org\/10.1016\/0304-3975(78)90020-8","DOI":"10.1016\/0304-3975(78)90020-8"},{"key":"24_CR15","doi-asserted-by":"crossref","unstructured":"Hague, M., Kochems, J., Ong, C.L.: Unboundedness and downward closures of higher-order pushdown automata. In: POPL 2016: Principles of Programming Languages. pp. 151\u2013163. ACM (2016)","DOI":"10.1145\/2914770.2837627"},{"key":"24_CR16","doi-asserted-by":"publisher","unstructured":"Hague, M., Murawski, A.S., Ong, C.L., Serre, O.: Collapsible pushdown automata and recursion schemes. In: Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24\u201327 June 2008, Pittsburgh, PA, USA. pp. 452\u2013461 (2008). https:\/\/doi.org\/10.1109\/LICS.2008.34","DOI":"10.1109\/LICS.2008.34"},{"key":"24_CR17","doi-asserted-by":"crossref","unstructured":"Haines, L.H.: On free monoids partially ordered by embedding. Journal of Combinatorial Theory 6(1), 94\u201398 (1969)","DOI":"10.1016\/S0021-9800(69)80111-0"},{"key":"24_CR18","unstructured":"Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to automata theory, languages, and computation, 3rd Edition. Pearson international edition, Addison-Wesley (2007)"},{"key":"24_CR19","doi-asserted-by":"crossref","unstructured":"Jantzen, M.: On the hierarchy of Petri net languages. RAIRO - Theoretical Informatics and Applications - Informatique Th\u00e9orique et Applications 13(1), 19\u201330 (1979), http:\/\/www.numdam.org\/item?id=ITA_1979__13_1_19_0","DOI":"10.1051\/ita\/1979130100191"},{"key":"24_CR20","doi-asserted-by":"crossref","unstructured":"Jhala, R., Majumdar, R.: Interprocedural analysis of asynchronous programs. In: POPL \u201907: Proc. 34th ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages. pp. 339\u2013350. ACM Press (2007)","DOI":"10.1145\/1190216.1190266"},{"key":"24_CR21","doi-asserted-by":"publisher","unstructured":"Kobayashi, N.: Types and higher-order recursion schemes for verification of higher-order programs. In: Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21\u201323, 2009. pp. 416\u2013428 (2009). https:\/\/doi.org\/10.1145\/1480881.1480933","DOI":"10.1145\/1480881.1480933"},{"key":"24_CR22","doi-asserted-by":"crossref","unstructured":"Kobayashi, N.: Inclusion between the frontier language of a non-deterministic recursive program scheme and the Dyck language is undecidable. Theoretical Computer Science 777, 409\u2013416 (2019).","DOI":"10.1016\/j.tcs.2018.09.035"},{"key":"24_CR23","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Ong, C.L.: Complexity of model checking recursion schemes for fragments of the modal mu-calculus. Logical Methods in Computer Science 7(4) (2011)","DOI":"10.2168\/LMCS-7(4:9)2011"},{"key":"24_CR24","doi-asserted-by":"publisher","unstructured":"van Leeuwen, J.: Effective constructions in well-partially-ordered free monoids. Discrete Mathematics 21(3), 237\u2013252 (1978). https:\/\/doi.org\/10.1016\/0012-365X(78)90156-5","DOI":"10.1016\/0012-365X(78)90156-5"},{"key":"24_CR25","unstructured":"Majumdar, R., Thinniyam, R.S., Zetzsche, G.: General decidability results for asynchronous shared-memory programs: Higher-order and beyond (2021), http:\/\/arxiv.org\/abs\/2101.08611"},{"key":"24_CR26","unstructured":"Maslov, A.: The hierarchy of indexed languages of an arbitrary level. Doklady Akademii Nauk 217(5), 1013\u20131016 (1974)"},{"key":"24_CR27","doi-asserted-by":"crossref","unstructured":"Mayr, R.: Undecidable problems in unreliable computations. Theoretical Computer Science 297(1\u20133), 337\u2013354 (2003)","DOI":"10.1016\/S0304-3975(02)00646-1"},{"key":"24_CR28","doi-asserted-by":"publisher","unstructured":"Ong, L.: Higher-order model checking: An overview. In: 30th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6\u201310, 2015. pp. 1\u201315 (2015). https:\/\/doi.org\/10.1109\/LICS.2015.9","DOI":"10.1109\/LICS.2015.9"},{"key":"24_CR29","unstructured":"Parys, P.: The complexity of the diagonal problem for recursion schemes. In: Proceedings of FSTTCS 2017. Leibniz International Proceedings in Informatics (LIPIcs), vol. 93, pp. 45:1\u201345:14 (2018)"},{"key":"24_CR30","doi-asserted-by":"crossref","unstructured":"Sen, K., Viswanathan, M.: Model checking multithreaded programs with asynchronous atomic methods. In: CAV \u201906: Proc. 18th Int. Conf. on Computer Aided Verification. LNCS, vol. 4144, pp. 300\u2013314. Springer (2006)","DOI":"10.1007\/11817963_29"},{"key":"24_CR31","unstructured":"Sipser, M.: Introduction to the theory of computation. PWS Publishing Company (1997)"},{"key":"24_CR32","doi-asserted-by":"publisher","unstructured":"Thinniyam, R.S., Zetzsche, G.: Regular separability and intersection emptiness are independent problems. In: Proceedings of FSTTCS 2019. Leibniz International Proceedings in Informatics (LIPIcs), vol. 150, pp. 51:1\u201351:15. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2019). https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2019.51","DOI":"10.4230\/LIPIcs.FSTTCS.2019.51"},{"key":"24_CR33","unstructured":"Zetzsche, G.: An approach to computing downward closures. In: ICALP 2015. vol. 9135, pp. 440\u2013451. Springer (2015), the undecidability of $$Z$$ intersection is shown in the full version: http:\/\/arxiv.org\/abs\/1503.01068"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-72016-2_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T00:11:26Z","timestamp":1616371886000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-72016-2_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720155","9783030720162"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72016-2_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"20 March 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"141","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"41","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"21","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference changed to an online format due to the COVID-19 pandemic","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}