{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:15:48Z","timestamp":1767928548911,"version":"3.49.0"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2022,10,21]],"date-time":"2022-10-21T00:00:00Z","timestamp":1666310400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000780","name":"European Commission","doi-asserted-by":"crossref","award":["610150"],"award-info":[{"award-number":["610150"]}],"id":[{"id":"10.13039\/501100000780","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>The model of asynchronous programming arises in many contexts, from low-level\nsystems software to high-level web programming. We take a language-theoretic\nperspective and show general decidability and undecidability results for\nasynchronous programs that capture all known results as well as show\ndecidability of new and important classes. As a main consequence, we show\ndecidability of safety, termination and boundedness verification for\nhigher-order asynchronous programs -- such as OCaml programs using Lwt -- and\nundecidability of liveness verification already for order-2 asynchronous\nprograms. We show that under mild assumptions, surprisingly, safety and\ntermination verification of asynchronous programs with handlers from a language\nclass are decidable iff emptiness is decidable for the underlying language\nclass. Moreover, we show that configuration reachability and liveness (fair\ntermination) verification are equivalent, and decidability of these problems\nimplies decidability of the well-known \"equal-letters\" problem on languages.\nOur results close the decidability frontier for asynchronous programs.<\/jats:p>","DOI":"10.46298\/lmcs-18(4:2)2022","type":"journal-article","created":{"date-parts":[[2022,10,24]],"date-time":"2022-10-24T12:15:02Z","timestamp":1666613702000},"source":"Crossref","is-referenced-by-count":2,"title":["General Decidability Results for Asynchronous Shared-Memory Programs: Higher-Order and Beyond"],"prefix":"10.46298","volume":"Volume 18, Issue 4","author":[{"given":"Rupak","family":"Majumdar","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"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":"25203","published-online":{"date-parts":[[2022,10,21]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/10187\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/10187\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T20:20:10Z","timestamp":1687292410000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/7606"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,21]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-18(4:2)2022","relation":{"has-preprint":[{"id-type":"arxiv","id":"2101.08611v1","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2101.08611","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2101.08611","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,10,21]]},"article-number":"7606"}}