{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T02:28:53Z","timestamp":1784255333391,"version":"3.55.0"},"reference-count":53,"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-sa\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["AdG 787914 FRAPPANT"],"award-info":[{"award-number":["AdG 787914 FRAPPANT"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["DFG RTG 2236 UnRAVeL"],"award-info":[{"award-number":["DFG RTG 2236 UnRAVeL"]}],"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 consider imperative programs that involve\n            <jats:italic toggle=\"yes\">both<\/jats:italic>\n            randomization\n            <jats:italic toggle=\"yes\">and<\/jats:italic>\n            pure nondeterminism. The central question is how to find a strategy resolving the pure nondeterminism such that the so-obtained\n            <jats:italic toggle=\"yes\">determinized<\/jats:italic>\n            program satisfies a given quantitative specification, i.e., bounds on expected outcomes such as the expected final value of a program variable or the probability to terminate in a given set of states. We show how\n            <jats:italic toggle=\"yes\">memoryless and deterministic (MD)<\/jats:italic>\n            strategies can be obtained in a semi-automatic fashion using deductive verification techniques. For loop-free programs, the MD strategies resulting from our weakest preconditionstyle framework are correct by construction. This extends to loopy programs, provided the loops are equipped with suitable loop invariants - just like in program verification. We show how our technique relates to the well-studied problem of obtaining strategies in countably infinite Markov decision processes with reachabilityreward objectives. Finally, we apply our technique to several case studies.\n          <\/jats:p>","DOI":"10.1145\/3632935","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"2792-2820","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8705-2564","authenticated-orcid":false,"given":"Kevin","family":"Batz","sequence":"first","affiliation":[{"name":"RWTH Aachen University, Aachen, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-0169-641X","authenticated-orcid":false,"given":"Tom Jannik","family":"Biskup","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Aachen, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6143-1926","authenticated-orcid":false,"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Aachen, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1084-6408","authenticated-orcid":false,"given":"Tobias","family":"Winkler","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Aachen, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10270-017-0626-5"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3365365.3382220"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1674-2"},{"key":"e_1_3_1_6_1","unstructured":"Christel Baier and Joost-Pieter Katoen. 2008. Principles of model checking. MIT Press."},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-03113185-1_3"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2311.06889arXiv:2311.06889"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30820-8_25"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_25"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527310"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434320"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290347"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571260"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.FSTTCS.2008.1741"},{"key":"e_1_3_1_16_1","first-page":"415","volume-title":"In Proceedings of the 5th Berkeley symposium on Mathematical Statistics and Probability","author":"Blackwell David","year":"1967","unstructured":"David Blackwell. 1967. Positive dynamic programming. In Proceedings of the 5th Berkeley symposium on Mathematical Statistics and Probability, Vol. 1. University of California Press Berkeley, 415-418."},{"key":"e_1_3_1_17_1","unstructured":"Craig Boutilier Raymond Reiter and Bob Price. 2001. Symbolic Dynamic Programming for First-Order MDPs. In IFCAI Morgan Kaufmann 690-700."},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1137\/1.9781611973075.70"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-11(2:16)2015"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699431"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2735960.2735973"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68167-2_26"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2012.21"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.PEVA.2017.09.005"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371105"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10009-021-00633-Z"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/11415787_21"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1460833.1460872"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.JCSS.2021.02.006"},{"key":"e_1_3_1_31_1","volume-title":"Advanced weakest precondition calculi for probabilistic programs","author":"Kaminski Benjamin Lucien","year":"2019","unstructured":"Benjamin Lucien Kaminski. 2019. Advanced weakest precondition calculi for probabilistic programs. Ph. D. Dissertation. RWTH Aachen University, Germany."},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/S00236-018-0321-1"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934574"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15769-1_24"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-54093900-9_17"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10703010-0097-6"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/800061.808758"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90012-1"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1014745904458"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46029-2_13"},{"key":"e_1_3_1_42_1","volume-title":"Specifying Systems, The TLA+Language and Tools for Hardware and Software Engineers","author":"Lamport Leslie","year":"2002","unstructured":"Leslie Lamport. 2002. Specifying Systems, The TLA+Language and Tools for Hardware and Software Engineers. Addison-Wesley."},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-1711-4_20"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-12(3:6)2016"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/b138392"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.3233\/978-1-61499-810-5-104"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.SCICO.2022.102822"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9939-1969-0253756-8"},{"key":"e_1_3_1_49_1","article-title":"Fixpoint Induction and Proofs of Program Properties","volume":"5","author":"Park David","year":"1969","unstructured":"David Park. 1969. Fixpoint Induction and Proofs of Program Properties. Machine intelligence 5 (1969).","journal-title":"Machine intelligence"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","unstructured":"Martin L. Puterman. 1994. Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley. https:\/\/doi.org\/10.1002\/9780470316887 10.1002\/9780470316887","DOI":"10.1002\/9780470316887"},{"key":"e_1_3_1_51_1","first-page":"643","volume-title":"In UAI","author":"Sanner Scott","year":"2011","unstructured":"Scott Sanner, Karina Valdivia Delgado, and Leliane Nunes de Barros. 2011. Symbolic Dynamic Programming for Discrete and Continuous State MDPs. In UAI. AUAI Press, 643-652."},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622870"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27645-3_1"},{"key":"e_1_3_1_54_1","unstructured":"Wikipedia. 2023. Nim - Wikipedia The Free Encyclopedia. http:\/\/en.wikipedia.org\/w\/index.php?title=Nim&oldid=1163491825. [Online; accessed 10-July-2023]."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632935","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632935","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:03:39Z","timestamp":1751659419000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632935"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":53,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632935"],"URL":"https:\/\/doi.org\/10.1145\/3632935","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"}}]}}