{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:31:55Z","timestamp":1784845915440,"version":"3.55.0"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2021,6,8]],"date-time":"2021-06-08T00:00:00Z","timestamp":1623110400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"CRECOGI"},{"DOI":"10.13039\/501100002241","name":"Japan Science and Technology Agency","doi-asserted-by":"publisher","award":["JPMJER1603"],"award-info":[{"award-number":["JPMJER1603"]}],"id":[{"id":"10.13039\/501100002241","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001691","name":"Japan Society for the Promotion of Science","doi-asserted-by":"crossref","award":["15KT0012 \/ 15K11984 \/ 16J08157"],"award-info":[{"award-number":["15KT0012 \/ 15K11984 \/ 16J08157"]}],"id":[{"id":"10.13039\/501100001691","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2021,6,30]]},"abstract":"<jats:p>\n            Computing reachability probabilities is a fundamental problem in the analysis of randomized programs. This article aims at a comprehensive and comparative account of various\n            <jats:italic>martingale-based methods<\/jats:italic>\n            for over- and under-approximating reachability probabilities. Based on the existing works that stretch across different communities (formal verification, control theory, etc.), we offer a unifying account. In particular, we emphasize the role of order-theoretic fixed points\u2014a classic topic in computer science\u2014in the analysis of randomized programs. This leads us to two new martingale-based techniques, too. We also make an experimental comparison using our implementation of template-based synthesis algorithms for those martingales.\n          <\/jats:p>","DOI":"10.1145\/3450967","type":"journal-article","created":{"date-parts":[[2021,6,8]],"date-time":"2021-06-08T16:09:23Z","timestamp":1623168563000},"page":"1-46","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":31,"title":["Ranking and Repulsing Supermartingales for Reachability in Randomized Programs"],"prefix":"10.1145","volume":"43","author":[{"given":"Toru","family":"Takisaka","sequence":"first","affiliation":[{"name":"National Institute of Informatics, Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yuichiro","family":"Oyabu","sequence":"additional","affiliation":[{"name":"National Institute of Informatics, Japan and The Graduate University for Advanced Studies (SOKENDAI), Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Natsuki","family":"Urabe","sequence":"additional","affiliation":[{"name":"National Institute of Informatics, Japan and University of Tokyo, Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ichiro","family":"Hasuo","sequence":"additional","affiliation":[{"name":"National Institute of Informatics, Japan and The Graduate University for Advanced Studies (SOKENDAI), Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,6,8]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.3166\/ejc.16.624-641"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158122"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15769-1_8"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/6490.6494"},{"key":"e_1_2_1_5_1","volume-title":"Rudiments of -Calculus","author":"Arnold Andr\u00e9","unstructured":"Andr\u00e9 Arnold and Damian Niwi\u0144ski. 2001. Rudiments of -Calculus. Elsevier."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-90686-7_9"},{"key":"e_1_2_1_7_1","volume-title":"Principles of Model Checking","author":"Baier Christel","unstructured":"Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. The MIT Press."},{"key":"e_1_2_1_8_1","volume-title":"Shreve","author":"Bertsekas Dimitri P.","year":"2007","unstructured":"Dimitri P. Bertsekas and Steven E. Shreve. 2007. Stochastic Optimal Control: The Discrete-Time Case. Athena Scientific."},{"key":"e_1_2_1_9_1","volume-title":"In Proceedings of the ACM SIGPLAN Symposium on Principles of Programming Languages. ACM.","author":"Bod\u00edk Rastislav","year":"2016","unstructured":"Rastislav Bod\u00edk and Rupak Majumdar (Eds.). 2016. In Proceedings of the ACM SIGPLAN Symposium on Principles of Programming Languages. ACM."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_15"},{"key":"e_1_2_1_12_1","volume-title":"Termination of nondeterministic recursive probabilistic programs. CoRR abs\/1701.02944","author":"Chatterjee Krishnendu","year":"2017","unstructured":"Krishnendu Chatterjee and Hongfei Fu. 2017. Termination of nondeterministic recursive probabilistic programs. CoRR abs\/1701.02944 (2017)."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_1"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837639"},{"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.2140\/pjm.1979.82.43"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677001"},{"key":"e_1_2_1_18_1","unstructured":"A. Makhorin. 2008. GLPK\u2013GNU Linear Programming Kit. http:\/\/www.gnu.org\/software\/glpk\/."},{"key":"e_1_2_1_19_1","volume-title":"Proceedings of the Conference on the Future of Software Engineering, (FOSE\u201914)","author":"Gordon Andrew D.","unstructured":"Andrew D. Gordon, Thomas A. Henzinger, Aditya V. Nori, and Sriram K. Rajamani. 2014. Probabilistic programming. In Proceedings of the Conference on the Future of Software Engineering, (FOSE\u201914), James D. Herbsleb and Matthew B. Dwyer (Eds.). ACM, 167\u2013181."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837673"},{"key":"e_1_2_1_21_1","volume-title":"Johnson","author":"Horn Roger A.","year":"2012","unstructured":"Roger A. Horn and Charles R. Johnson. 2012. Matrix Analysis (2nd ed.). Cambridge University Press, New York, NY."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46541-3_24"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the 17th International Symposium on Static Analysis (SAS\u201910)","author":"Katoen Joost-Pieter","unstructured":"Joost-Pieter Katoen, Annabelle McIver, Larissa Meinicke, and Carroll C. Morgan. 2010. Linear-invariant generation for probabilistic programs: Automated support for proof-based methods. In Proceedings of the 17th International Symposium on Static Analysis (SAS\u201910). 390\u2013406."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90012-1"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","unstructured":"Satoshi Kura Natsuki Urabe and Ichiro Hasuo. 2019. Tail probabilities for randomized program runtimes via martingales for higher moments. In Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201919) Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS\u201919) (Lecture Notes in Computer Science) Tom\u00e1s Vojnar and Lijun Zhang (Eds.) Vol. 11428. Springer 135\u2013153. DOI:https:\/\/doi.org\/10.1007\/978-3-030-17465-1_8","DOI":"10.1007\/978-3-030-17465-1_8"},{"key":"e_1_2_1_27_1","volume-title":"Refinement and Proof for Probabilistic Systems (Monographs in Computer Science)","author":"McIver Annabelle","unstructured":"Annabelle McIver and Carroll Morgan. 2004. Abstraction, Refinement and Proof for Probabilistic Systems (Monographs in Computer Science). SpringerVerlag."},{"key":"e_1_2_1_28_1","volume-title":"Proceedings of the 1st Pernambuco Summer School on Software Engineering: Refinement Techniques in Software Engineering (PSSE\u201904) (LNCS)","author":"McIver Annabelle","unstructured":"Annabelle McIver and Carroll Morgan. 2004. Developing and reasoning about probabilistic programs in pGCL. In Proceedings of the 1st Pernambuco Summer School on Software Engineering: Refinement Techniques in Software Engineering (PSSE\u201904) (LNCS), Ana Cavalcanti, Augusto Sampaio, and Jim Woodcock (Eds.), Vol. 3167. Springer, 123\u2013155."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158121"},{"key":"e_1_2_1_30_1","volume-title":"Fifty Challenging Problems in Probability with Solutions","author":"Mosteller Frederick","unstructured":"Frederick Mosteller. 2012. Fifty Challenging Problems in Probability with Solutions. Dover Publications."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-74759-0_405"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192394"},{"key":"e_1_2_1_33_1","volume-title":"Proceedings of the 43rd IEEE Conference on Decision and Control. IEEE","author":"Prajna Stephen","unstructured":"Stephen Prajna, Ali Jadbabaie, and George J. Pappas. 2004. Stochastic safety verification using barrier certificates. In Proceedings of the 43rd IEEE Conference on Decision and Control. IEEE, Piscataway, NJ, 929\u2013934."},{"key":"e_1_2_1_34_1","volume-title":"The K-moment problem for compact semi-algebraic sets. Math. Ann. 289, 1 (01","author":"Schm\u00fcdgen Konrad","year":"1991","unstructured":"Konrad Schm\u00fcdgen. 1991. The K-moment problem for compact semi-algebraic sets. Math. Ann. 289, 1 (01 Mar. 1991), 203\u2013206."},{"key":"e_1_2_1_35_1","volume-title":"Theory of Linear and Integer Programming","author":"Schrijver Alexander","unstructured":"Alexander Schrijver. 1998. Theory of Linear and Integer Programming. Wiley."},{"key":"e_1_2_1_36_1","volume-title":"SDPT3\u2013a Matlab software package for semidefinite programming. Optimization Methods and Software 11","author":"Toh K. C.","year":"1999","unstructured":"K. C. Toh, M. J. Todd, and R. H. Tutuncu, SDPT3\u2013a Matlab software package for semidefinite programming. Optimization Methods and Software 11 (1999), 545\u2013581."},{"key":"e_1_2_1_37_1","volume-title":"Parrilo","author":"Papachristodoulou Antonis","year":"2013","unstructured":"Antonis Papachristodoulou, James Anderson, Giorgio Valmorbida, Stephen Prajna, Pete Seiler, and Pablo A. Parrilo. 2013. SOSTOOLS Version 3.00 Sum of Squares Optimization Toolbox for MATLAB. CoRR abs\/1310.4716."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1177\/0278364912444146"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-01090-4_28"},{"key":"e_1_2_1_40_1","volume-title":"A Decision Method for Elementary Algebra and Geometry","author":"Tarski Alfred","unstructured":"Alfred Tarski. 1951. A Decision Method for Elementary Algebra and Geometry. University of California Press, Berkeley."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005151"},{"key":"e_1_2_1_42_1","volume-title":"Proceedings of the Banff Higher Order Workshop (Lecture Notes in Computer Science), Faron Moller and Graham M. Birtwistle (Eds.)","volume":"1043","author":"Vardi Moshe Y.","year":"1995","unstructured":"Moshe Y. Vardi. 1995. An automata-theoretic approach to linear temporal logic. In Proceedings of the Banff Higher Order Workshop (Lecture Notes in Computer Science), Faron Moller and Graham M. Birtwistle (Eds.), Vol. 1043. Springer, 238\u2013266."}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3450967","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3450967","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3450967","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T17:49:24Z","timestamp":1750268964000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3450967"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6,8]]},"references-count":42,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2021,6,30]]}},"alternative-id":["10.1145\/3450967"],"URL":"https:\/\/doi.org\/10.1145\/3450967","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,6,8]]},"assertion":[{"value":"2019-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-02-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-06-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}