{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T23:08:52Z","timestamp":1740179332066,"version":"3.37.3"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["389792660"],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,1,5]]},"abstract":"\n We study the recursion-theoretic complexity of Positive Almost-Sure Termination (\n PAST<\/jats:italic>\n ) in an imperative programming language with rational variables, bounded nondeterministic choice, and discrete probabilistic choice. A program terminates positive almost-surely if, for every scheduler, the program terminates almost-surely and the expected runtime to termination is finite. We show that\n PAST<\/jats:italic>\n for our language is complete for the (lightface) co-analytic sets (\u03a0\n 1<\/jats:sub>\n 1<\/jats:sup>\n -complete). This is in contrast to the related notions of Almost-Sure Termination (\n AST<\/jats:italic>\n ) and Bounded Termination (\n BAST<\/jats:italic>\n ), both of which are arithmetical (\u03a0\n 2<\/jats:sub>\n 0<\/jats:sup>\n - and \u03a3\n 2<\/jats:sub>\n 0<\/jats:sup>\n -complete respectively).\n <\/jats:p>\n \n Our upper bound implies an effective procedure to reduce reasoning about probabilistic termination to non-probabilistic fair termination in a model with bounded nondeterminism, and to simple program termination in models with unbounded nondeterminism. Our lower bound shows the opposite: for every program with unbounded nondeterministic choice, there is an effectively computable probabilistic program with bounded choice such that the original program is terminating if, and only if, the transformed program is\n PAST<\/jats:italic>\n .\n <\/jats:p>\n \n We show that every program has an effectively computable normal form, in which each probabilistic choice either continues or terminates execution immediately, each with probability 1\/2. For normal form programs, we provide a sound and complete proof rule for\n PAST<\/jats:italic>\n . Our proof rule uses transfinite ordinals. We show that reasoning about\n PAST<\/jats:italic>\n requires transfinite ordinals up to \u03c9\n 1<\/jats:sub>\n \n CK<\/jats:italic>\n <\/jats:sup>\n ; thus, existing techniques for probabilistic termination based on ranking supermartingales that map program states to reals do not suffice to reason about\n PAST<\/jats:italic>\n .\n <\/jats:p>","DOI":"10.1145\/3632879","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"1089-1117","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Positive Almost-Sure Termination: Complexity and Proof Rules"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2136-0542","authenticated-orcid":false,"given":"Rupak","family":"Majumdar","sequence":"first","affiliation":[{"name":"Max Planck Institute for Software Systems, Kaiserslautern, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-5187-5415","authenticated-orcid":false,"given":"V. R.","family":"Sathiyanarayana","sequence":"additional","affiliation":[{"name":"Max Planck Institute for Software Systems, Kaiserslautern, Germany"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/295656.295659"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/6490.6494"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2019.102338"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434320"},{"key":"e_1_2_1_5_1","volume-title":"Shreve","author":"Bertsekas Dmitri P.","year":"1978","unstructured":"Dmitri P. Bertsekas and Steven E. Shreve. 1978. Stochastic Optimal Control: The Discrete Time Case. Academic Press."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454111"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_24"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_34"},{"volume-title":"Foundations of Computer Science (FOCS)","author":"Chandra Ashok","key":"e_1_2_1_9_1","unstructured":"Ashok Chandra. 1978. Computable nondeterministic functions. In Foundations of Computer Science (FOCS). IEEE, 127\u2013131."},{"key":"e_1_2_1_10_1","unstructured":"Krishnendu Chatterjee and Hongfei Fu. 2017. Termination of Nondeterministic Recursive Probabilistic Programs. arxiv:1701.02944."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_1"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3174800"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13185-1_4"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-90870-6_33"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009873"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_39"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_4"},{"key":"e_1_2_1_18_1","unstructured":"Edsger Wybe Dijkstra. 1976. A discipline of programming. 613924118 prentice-hall Englewood Cliffs."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677001"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","unstructured":"Nissim Francez. 1986. Fairness. Springer. isbn:978-3-540-96235-9 https:\/\/doi.org\/10.1007\/978-1-4612-4886-6 10.1007\/978-1-4612-4886-6","DOI":"10.1007\/978-1-4612-4886-6"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-11245-5_22"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/4904.4993"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(84)80045-5"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-02768-1_11"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-018-0321-1"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3208102"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-23506-6_4"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1112\/blms\/14.4.285"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/1-84628-477-5"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17465-1_8"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_29"},{"key":"e_1_2_1_32_1","unstructured":"Rupak Majumdar and V. R. Sathiyanarayana. 2023. Positive Almost-Sure Termination \u2013 Complexity and Proof Rules. arxiv:2310.16145."},{"volume-title":"Mathematical Theory of Computation","author":"Manna Zohar","key":"e_1_2_1_33_1","unstructured":"Zohar Manna. 1974. Mathematical Theory of Computation. McGraw-Hill. isbn:9780070399105 lccn:73012753 https:\/\/books.google.de\/books?id=D7omAAAAMAAJ"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/b138392"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158121"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_18"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935317"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/800061.808757"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01458701"},{"key":"e_1_2_1_40_1","volume-title":"Theory of recursive functions and effective computability (Reprint from","author":"Hartley Rogers Jr..","year":"1967","unstructured":"Hartley Rogers Jr.. 1987. Theory of recursive functions and effective computability (Reprint from 1967). MIT Press. isbn:978-0-262-68052-3 https:\/\/mitpress.mit.edu\/9780262680523\/theory-of-recursive-functions-and-effective-computability\/"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3450967"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632879","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,29]],"date-time":"2024-01-29T15:17:29Z","timestamp":1706541449000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632879"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,5]]},"references-count":42,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,5]]}},"alternative-id":["10.1145\/3632879"],"URL":"https:\/\/doi.org\/10.1145\/3632879","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2024,1,5]]},"assertion":[{"value":"2024-01-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}