{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:06:02Z","timestamp":1784199962335,"version":"3.55.0"},"reference-count":50,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T00:00:00Z","timestamp":1749772800000},"content-version":"vor","delay-in-days":3,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-2008083"],"award-info":[{"award-number":["CCF-2008083"]}],"id":[{"id":"10.13039\/100000001","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":[[2025,6,10]]},"abstract":"<jats:p>We introduce a version of probabilistic Kleene algebra with angelic nondeterminism and a corresponding class of automata. Our approach implements semantics via distributions over multisets in order to overcome theoretical barriers arising from the lack of a distributive law between the powerset and Giry monads. We produce a full Kleene theorem and a coalgebraic theory, as well as both operational and denotational semantics and equational reasoning principles.<\/jats:p>","DOI":"10.1145\/3729286","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"897-919","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Probabilistic Kleene Algebra with Angelic Nondeterminism"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-6446-9680","authenticated-orcid":false,"given":"Shawn","family":"Ong","sequence":"first","affiliation":[{"name":"Cornell University, Ithaca, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-2786-2638","authenticated-orcid":false,"given":"Stephanie","family":"Ma","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8007-4725","authenticated-orcid":false,"given":"Dexter","family":"Kozen","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_3_2_2_2","volume-title":"Handbook of Logic in Computer Science","author":"Samson Abramsky","year":"1994","unstructured":"Samson Abramsky and Achim Jung. 1994. Domain theory. In Handbook of Logic in Computer Science, S. Abramsky, D.M. Gabbay, and T.S.E. Maibaum (Eds.). Vol. III. Oxford University Press."},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796821000137"},{"key":"e_1_3_2_4_2","volume-title":"The Lambda Calculus: Its Syntax and Semantics.","author":"Henk Barendregt","year":"1984","unstructured":"Henk Barendregt. 1984. The Lambda Calculus: Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics, Vol. 103. North-Holland."},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0048939"},{"key":"e_1_3_2_6_2","unstructured":"Merve Nur Cakir Mehwish Saleemi and Karl-Heinz Zimmermann. 2021. On the Theory of Stochastic Automata. CoRR abs\/2103.14423 (2021). arXiv:2103.14423 https:\/\/arxiv.org\/abs\/2103.14423"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_30"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-02508-3_9"},{"key":"e_1_3_2_9_2","volume-title":"A Monadic Theory of Point Processes.","author":"Swaraj Dash","year":"2023","unstructured":"Swaraj Dash. 2023. A Monadic Theory of Point Processes. Ph.D. Dissertation. Oxford University."},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.333.2"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.351.3"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)82521-6"},{"key":"e_1_3_2_13_2","first-page":"105","article-title":"On generative parallel composition","author":"D'Argenio P.","year":"1998","unstructured":"P.D'Argenio, H. Hermanns, and J.-P. Katoen. 1998. On generative parallel composition. In Proc. PROBMIV'98 (Electronic Notes in Theoretical ComputerScience, Vol. 22). 105\u2013122.","journal-title":"Proc. PROBMIV'98 (Electronic Notes in Theoretical ComputerScience, Vol. 22)"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_12"},{"key":"e_1_3_2_15_2","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/978-3-540-78913-0_10","volume-title":"Relations and Kleene Algebra in Computer Science","author":"Hitoshi Furusawa","year":"2008","unstructured":"Hitoshi Furusawa, Norihiro Tsumagari, and Koki Nishizawa. 2008. A Non-probabilistic Relational Model of Probabilistic Kleene Algebras. In Relations and Kleene Algebra in Computer Science, Rudolf Berghammer, Bernhard M\u00f6ller, and Georg Struth (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 110\u2013122."},{"key":"e_1_3_2_16_2","first-page":"68","volume-title":"Categorical Aspects of Topology and Analysis (Lecture Notes In Mathematics, 915)","author":"Giry M.","year":"1981","unstructured":"M. Giry. 1981. A Categorical Approach to Probability Theory. In Categorical Aspects of Topology and Analysis (Lecture Notes In Mathematics, 915), B. Banaschewski (Ed.). Springer-Verlag, 68\u201385."},{"key":"e_1_3_2_17_2","first-page":"130","article-title":"Reactive, generative, and stratified models of probabilistic processes","author":"Glabbeek R.v.","year":"1990","unstructured":"R.v. Glabbeek, S. Smolka, B. Steffen, and C. Tofts. 1990. Reactive, generative, and stratified models of probabilistic processes. In Proc. LICS, IEEE. 130\u2013141.","journal-title":"Proc. LICS, IEEE"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394795"},{"key":"e_1_3_2_19_2","volume-title":"Proc. Joint Meeting of the 23rd EACSL Conf Computer Science Logic (CSL 2014) and 29th ACM\/IEEE Symp. Logic in Computer Science (LICS 2014),","author":"Niels Bjorn Bugge Grathwohl","year":"2014","unstructured":"Niels Bjorn Bugge Grathwohl, Dexter Kozen, and Konstantinos Mamouras. 2014. KAT + B!. In Proc. Joint Meeting of the 23rd EACSL Conf Computer Science Logic (CSL 2014) and 29th ACM\/IEEE Symp. Logic in Computer Science (LICS 2014), Matthias Baaz, Thomas Eiter, and Helmut Veith (Eds.). EACSL and ACM\/IEEE, Vienna, Austria."},{"issue":"1994","key":"e_1_3_2_20_2","article-title":"Time and probability in formal design of distributed systems","volume":"1","author":"Hansson H.","year":"1994","unstructured":"H. Hansson. 1994. Time and probability in formal design of distributed systems. Real-Time Safety Critical Systems 1 (1994).","journal-title":"Real-Time Safety Critical Systems"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.22028\/D291-26690"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45804-2"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470678"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-13(1:2)2017"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/256167.256195"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","unstructured":"Dexter Kozen and Alexandra Silva. 2017. Practical coinduction. Mathematical Structures in Computer Science 27 (2017) 1132-1152. doi:10.1017\/S0960129515000493","DOI":"10.1017\/S0960129515000493"},{"key":"e_1_3_2_27_2","first-page":"244","volume-title":"Proc. 10th Int. Workshop Computer Science Logic (CSL'96) (Lecture Notes in Computer Science, Vol. 1258),","author":"Dexter Kozen","year":"1996","unstructured":"Dexter Kozen and Frederick Smith. 1996. Kleene algebra with tests: Completeness and decidability. In Proc. 10th Int. Workshop Computer Science Logic (CSL'96) (Lecture Notes in Computer Science, Vol. 1258), D. van Dalen and M. Bezem (Eds.). Springer-Verlag, Utrecht, The Netherlands, 244\u2013259."},{"issue":"1968","key":"e_1_3_2_28_2","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/BF01110627","article-title":"A fixpoint theorem for complete categories","volume":"103","author":"Joachim Lambek","year":"1968","unstructured":"Joachim Lambek. 1968. A fixpoint theorem for complete categories. Mathematische Zeitschrift 103 (1968), 151\u2013161.","journal-title":"Mathematische Zeitschrift"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90030-6"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2007.10.005"},{"key":"e_1_3_2_31_2","doi-asserted-by":"crossref","first-page":"264","DOI":"10.1007\/978-3-642-21070-9_20","volume-title":"Relational and Algebraic Methods in Computer Science","author":"Annabelle McIver","year":"2011","unstructured":"Annabelle McIver, Tahiry M. Rabehaja, and Georg Struth. 2011. On Probabilistic Kleene Algebras, Automata and Simulations. In Relational and Algebraic Methods in Computer Science, Harrie de Swart (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 264\u2013279."},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/11828563_20"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44618-4_26"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.04.019"},{"key":"e_1_3_2_35_2","volume-title":"Probability and Angelic Nondeterminism with Multiset Semantics. Technical Report","author":"Shawn Ong","year":"2024","unstructured":"Shawn Ong, Stephanie Ma, and Dexter Kozen. 2024. Probability and Angelic Nondeterminism with Multiset Semantics. Technical Report https:\/\/arxiv.org\/abs\/2412.06754. Cornell University."},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1993.1012"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1109\/ISCC.2008.4625616"},{"key":"e_1_3_2_38_2","unstructured":"Mathys Rennela. 2016. Convexity and Order in Probabilistic Call-by-Name FPC. CoRR abs\/1607.04332 (2016). arXiv:1607.04332 http:\/\/arxiv.org\/abs\/1607.04332"},{"key":"e_1_3_2_39_2","doi-asserted-by":"crossref","first-page":"234","DOI":"10.1007\/3-540-60218-6_17","volume-title":"CONCUR \u201895: Concurrency Theory","author":"Roberto Segala","year":"1995","unstructured":"Roberto Segala. 1995. A compositional trace-based semantics for probabilistic automata. In CONCUR \u201895: Concurrency Theory, Insup Lee and Scott A. Smolka (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 234\u2013248."},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.5555\/922031"},{"key":"e_1_3_2_41_2","first-page":"481","volume-title":"Proc. CONCUR (LNCS, Vol. 836).","author":"Segala R.","year":"1994","unstructured":"R. Segala and N. Lynch. 1994. Probabilistic simulations for probabilistic processes. In Proc. CONCUR (LNCS, Vol. 836). Springer, 481\u2013496."},{"key":"e_1_3_2_42_2","volume-title":"Kleene Coalgebra","author":"Alexandra Silva","year":"2010","unstructured":"Alexandra Silva. 2010. Kleene Coalgebra. Ph. D. Dissertation. University of Nijmegen."},{"key":"e_1_3_2_43_2","article-title":"Cantor meets Scott: Domain- Theoretic Foundations for Probabilistic Network Programming","author":"Steffen Smolka","year":"2016","unstructured":"Steffen Smolka, Praveen Kumar, Nate Foster, Dexter Kozen, and Alexandra Silva. 2016. Cantor meets Scott: Domain- Theoretic Foundations for Probabilistic Network Programming. CoRR abs\/1607.05830 (2016). arXiv:1607.05830 http:\/\/arxiv.org\/abs\/1607.05830","journal-title":"CoRR abs\/1607.05830 (2016)"},{"issue":"2011","key":"e_1_3_2_44_2","doi-asserted-by":"crossref","first-page":"5095","DOI":"10.1016\/j.tcs.2011.05.008","article-title":"Probabilistic systems coalgebraically: A survey","volume":"412","author":"Ana Sokolova","year":"2011","unstructured":"Ana Sokolova. 2011. Probabilistic systems coalgebraically: A survey. Theoretical Computer Science 412 (2011), 5095-5110.","journal-title":"Theoretical Computer Science"},{"key":"e_1_3_2_45_2","volume-title":"Probability, nondeterminism and concurrency: Two denotational models for probabilistic computation","author":"Daniele Varacca","year":"2003","unstructured":"Daniele Varacca. 2003. Probability, nondeterminism and concurrency: Two denotational models for probabilistic computation. Ph. D. Dissertation. Aarhus University."},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129505005074"},{"key":"e_1_3_2_47_2","first-page":"327","article-title":"Automatic verification of probabilistic concurrent finite state programs","author":"Vardi M.","year":"1985","unstructured":"M. Vardi. 1985. Automatic verification of probabilistic concurrent finite state programs. In Proc. FOCS, IEEE. 327\u2013338.","journal-title":"Proc. FOCS, IEEE."},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2019.09.016"},{"key":"e_1_3_2_49_2","volume-title":"A Demonic Outcome Logic for Randomized Nondeterminism. Technical Report","author":"Noam Zilberstein","year":"2024","unstructured":"Noam Zilberstein, Dexter Kozen, Alexandra Silva, and Joseph Tassarotti. 2024. A Demonic Outcome Logic for Randomized Nondeterminism. Technical Report https:\/\/arxiv.org\/abs\/2410.22540. Cornell University. POPL 2025, to appear."},{"key":"e_1_3_2_50_2","volume-title":"On the non-compositionality of monads via distributive laws.","author":"Maaike Zwart","year":"2020","unstructured":"Maaike Zwart. 2020. On the non-compositionality of monads via distributive laws. Ph. D. Dissertation. Oxford University."},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-18(1:13)2022"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729286","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729286","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:06:02Z","timestamp":1784196362000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729286"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":50,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3729286"],"URL":"https:\/\/doi.org\/10.1145\/3729286","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-14","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}