{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T08:26:14Z","timestamp":1770279974259,"version":"3.49.0"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["389792660"],"award-info":[{"award-number":["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,2]]},"abstract":"<jats:p>\n            We study the recursion-theoretic complexity of Positive Almost-Sure Termination (PAST) 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 PAST for our language is complete for the (lightface) co-analytic sets (\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:msubsup>\n                  <mml:mo>\u03a0<\/mml:mo>\n                  <mml:mn>1<\/mml:mn>\n                  <mml:mn>1<\/mml:mn>\n                <\/mml:msubsup>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            -complete). This is in contrast to the related notions of Almost-Sure Termination (AST) and Bounded Termination (BAST), both of which are arithmetical (\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:msubsup>\n                  <mml:mo>\u03a0<\/mml:mo>\n                  <mml:mn>2<\/mml:mn>\n                  <mml:mn>0<\/mml:mn>\n                <\/mml:msubsup>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            - and\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:msubsup>\n                  <mml:mo>\u03a3<\/mml:mo>\n                  <mml:mn>2<\/mml:mn>\n                  <mml:mn>0<\/mml:mn>\n                <\/mml:msubsup>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            -complete respectively).\n          <\/jats:p>\n          <jats:p>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 PAST.<\/jats:p>\n          <jats:p>\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\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mrow>\n                  <mml:mn>1<\/mml:mn>\n                  <mml:mo>\/<\/mml:mo>\n                  <mml:mn>2<\/mml:mn>\n                <\/mml:mrow>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            . For normal form programs, we provide a sound and complete proof rule for PAST. Our proof rule uses transfinite ordinals. We show that reasoning about PAST requires transfinite ordinals up to\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mrow>\n                  <mml:msubsup>\n                    <mml:mi>\u03c9<\/mml:mi>\n                    <mml:mn>1<\/mml:mn>\n                    <mml:mrow>\n                      <mml:mtext>CK<\/mml:mtext>\n                    <\/mml:mrow>\n                  <\/mml:msubsup>\n                <\/mml:mrow>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            ; thus, existing techniques for probabilistic termination based on ranking supermartingales that map program states to reals do not suffice to reason about PAST.\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":10,"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_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/295656.295659"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/6490.6494"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2019.102338"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434320"},{"key":"e_1_3_1_6_1","unstructured":"Dmitri P. Bertsekas and Steven E. Shreve. 1978. Stochastic Optimal Control: The Discrete Time Case. Academic Press"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454111"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_24"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1978.10"},{"key":"e_1_3_1_11_1","unstructured":"Krishnendu Chatterjee and Hongfei Fu. 2017. Termination of Nondeterministic Recursive Probabilistic Programs.[arxiv]1701. 02944 [cs.PL]."},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_1"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3174800"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13185-1_4"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-90870-6_33"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009873"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_39"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_4"},{"key":"e_1_3_1_19_1","volume-title":"A discipline of programming","author":"Edsger Wybe Dijkstra","year":"1976","unstructured":"Edsger Wybe Dijkstra. 1976. A discipline of programming. Vol. 613924118. prentice-hall Englewood Cliffs."},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677001"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4886-6"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-11245-5_22"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/4904.4993"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(84)80045-5"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-02768-1_11"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-018-0321-1"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3208102"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-23506-6_4"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1112\/blms\/14.4.285"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/1-84628-477-5"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17465-1_8"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_29"},{"key":"e_1_3_1_33_1","unstructured":"Rupak Majumdar and V. R. Sathiyanarayana. 2023. Positive Almost-Sure Termination \u2013 Complexity and Proof Rules. [arxiv]2310. 16145 [cs.PL]."},{"key":"e_1_3_1_34_1","unstructured":"Zohar Manna 1974. Mathematical Theory of Computation. McGraw-Hill. https:\/\/books.google.de\/books?id=D7omAAAAMAAJ"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/b138392"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158121"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_18"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","unstructured":"Federico Olmedo Benjamin Lucien Kaminski Joost-Pieter Katoen and Christoph Matheja. 2016. Reasoning about Recursive Probabilistic Programs.In Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science LICS '16 New York NY USA July 5\u20138 2016 Martin Grohe Eric Koskinen and Natarajan Shankar (Eds.). ACM 672\u2013681. https:\/\/doi.org\/10.1145\/2933575.2935317 10.1145\/2933575.2935317","DOI":"10.1145\/2933575.2935317"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/800061.808757"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01458701"},{"key":"e_1_3_1_41_1","volume-title":"Theory of recursive functions and effective computability (Reprint from 1967)","author":"Rogers Jr Hartley","year":"1987","unstructured":"Hartley Rogers Jr. 1987. Theory of recursive functions and effective computability (Reprint from 1967). MIT Press. https:\/\/mitpress.mit.edu\/9780262680523\/theory-of-recursive-functions-and-effective-computability\/"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3450967"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s2-42.1.230"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632879","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632879","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:07:13Z","timestamp":1751659633000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632879"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":42,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632879"],"URL":"https:\/\/doi.org\/10.1145\/3632879","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}