More Web Proxy on the site http://driver.im/

research-article

Open access

Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs

Authors:

Tom Jannik Biskup,

Joost-Pieter Katoen,

Tobias WinklerAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 8, Issue POPL

Article No.: 93, Pages 2792 - 2820

https://doi.org/10.1145/3632935

Published: 05 January 2024 Publication History

Abstract

We consider imperative programs that involve both randomization and pure nondeterminism. The central question is how to find a strategy resolving the pure nondeterminism such that the so-obtained determinized 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 memoryless and deterministic (MD) strategies can be obtained in a semi-automatic fashion using deductive verification techniques. For loop-free programs, the MD strategies resulting from our weakest precondition-style 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 reachability-reward objectives. Finally, we apply our technique to several case studies.

References

[1]

Jean-Raymond Abrial. 2010. Modeling in Event-B - System and Software Engineering. Cambridge University Press. https://doi.org/10.1017/CBO9781139195881

[2]

Mohamed Amine Aouadhi, Benoît Delahaye, and Arnaud Lanoix. 2019. Introducing probabilistic reasoning within Event-B. Softw. Syst. Model., 18, 3 (2019), 1953–1984. https://doi.org/10.1007/S10270-017-0626-5

[3]

Pranav Ashok, Mathias Jackermeier, Pushpak Jagtap, Jan Kretínský, Maximilian Weininger, and Majid Zamani. 2020. dtControl: decision tree learning algorithms for controller representation. In HSCC. ACM, 17:1–17:7. https://doi.org/10.1145/3365365.3382220

[4]

Ralph-Johan Back and Joakim von Wright. 1998. Refinement Calculus - A Systematic Introduction. Springer. https://doi.org/10.1007/978-1-4612-1674-2

[5]

Christel Baier and Joost-Pieter Katoen. 2008. Principles of model checking. MIT Press.

[6]

Jialu Bao, Nitesh Trivedi, Drashti Pathak, Justin Hsu, and Subhajit Roy. 2022. Data-Driven Invariant Learning for Probabilistic Programs. In CAV (1) (Lecture Notes in Computer Science, Vol. 13371). Springer, 33–54. https://doi.org/10.1007/978-3-031-13185-1_3

[7]

Kevin Batz, Tom Jannik Biskup, Joost-Pieter Katoen, and Tobias Winkler. 2023. Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs. https://doi.org/10.48550/ARXIV.2311.06889 arxiv:2311.06889.

[8]

Kevin Batz, Mingshuai Chen, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. 2023. Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants. In TACAS (2) (Lecture Notes in Computer Science, Vol. 13994). Springer, 410–429. https://doi.org/10.1007/978-3-031-30820-8_25

[9]

Kevin Batz, Mingshuai Chen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Philipp Schröer. 2021. Latticed k-Induction with an Application to Probabilistic Programs. In CAV (2) (Lecture Notes in Computer Science, Vol. 12760). Springer, 524–549. https://doi.org/10.1007/978-3-030-81688-9_25

[10]

Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Tobias Winkler. 2022. Weighted programming: a programming paradigm for specifying mathematical models. Proc. ACM Program. Lang., 6, OOPSLA1 (2022), 1–30. https://doi.org/10.1145/3527310

[11]

Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. 2021. Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning. Proc. ACM Program. Lang., 5, POPL (2021), 1–30. https://doi.org/10.1145/3434320

[12]

Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Thomas Noll. 2019. Quantitative separation logic: a logic for reasoning about probabilistic pointer programs. Proc. ACM Program. Lang., 3, POPL (2019), 34:1–34:29. https://doi.org/10.1145/3290347

[13]

Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Lena Verscht. 2023. A Calculus for Amortized Expected Runtimes. Proc. ACM Program. Lang., 7, POPL (2023), 1957–1986. https://doi.org/10.1145/3571260

[14]

Noam Berger, Nevin Kapur, Leonard J. Schulman, and Vijay V. Vazirani. 2008. Solvency Games. In FSTTCS (LIPIcs, Vol. 2). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 61–72. https://doi.org/10.4230/LIPICS.FSTTCS.2008.1741

[15]

David Blackwell. 1967. Positive dynamic programming. In Proceedings of the 5th Berkeley symposium on Mathematical Statistics and Probability. 1, 415–418.

[16]

Craig Boutilier, Raymond Reiter, and Bob Price. 2001. Symbolic Dynamic Programming for First-Order MDPs. In IJCAI. Morgan Kaufmann, 690–700.

[17]

Tomás Brázdil, Václav Brozek, Kousha Etessami, Antonín Kucera, and Dominik Wojtczak. 2010. One-Counter Markov Decision Processes. In SODA. SIAM, 863–874. https://doi.org/10.1137/1.9781611973075.70

[18]

Edsger W. Dijkstra. 1975. Guarded Commands, Nondeterminacy and Formal Derivation of Programs. Commun. ACM, 18, 8 (1975), 453–457.

[19]

Klaus Dräger, Vojtech Forejt, Marta Z. Kwiatkowska, David Parker, and Mateusz Ujma. 2015. Permissive Controller Synthesis for Probabilistic Systems. Log. Methods Comput. Sci., 11, 2 (2015), https://doi.org/10.2168/LMCS-11(2:16)2015

[20]

Kousha Etessami and Mihalis Yannakakis. 2015. Recursive Markov Decision Processes and Recursive Stochastic Games. J. ACM, 62, 2 (2015), 11:1–11:69. https://doi.org/10.1145/2699431

[21]

Lu Feng, Clemens Wiltsche, Laura R. Humphrey, and Ufuk Topcu. 2015. Controller synthesis for autonomous systems interacting with human operators. In ICCPS. ACM, 70–79. https://doi.org/10.1145/2735960.2735973

[22]

Yijun Feng, Lijun Zhang, David N. Jansen, Naijun Zhan, and Bican Xia. 2017. Finding Polynomial Loop Invariants for Probabilistic Programs. In ATVA (Lecture Notes in Computer Science, Vol. 10482). Springer, 400–416. https://doi.org/10.1007/978-3-319-68167-2_26

[23]

Friedrich Gretz, Joost-Pieter Katoen, and Annabelle McIver. 2012. Operational Versus Weakest Precondition Semantics for the Probabilistic Guarded Command Language. In QEST. IEEE Computer Society, 168–177. https://doi.org/10.1109/QEST.2012.21

[24]

Sofie Haesaert, Nathalie Cauchi, and Alessandro Abate. 2017. Certified policy synthesis for general Markov decision processes: An application in building automation systems. Perform. Evaluation, 117 (2017), 75–103. https://doi.org/10.1016/J.PEVA.2017.09.005

[25]

Marcel Hark, Benjamin Lucien Kaminski, Jürgen Giesl, and Joost-Pieter Katoen. 2020. Aiming low is harder: induction for lower bounds in probabilistic program verification. Proc. ACM Program. Lang., 4, POPL (2020), 37:1–37:28. https://doi.org/10.1145/3371105

[26]

Christian Hensel, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann, and Matthias Volk. 2022. The probabilistic model checker Storm. Int. J. Softw. Tools Technol. Transf., 24, 4 (2022), 589–610. https://doi.org/10.1007/S10009-021-00633-Z

[27]

Thai Son Hoang, Zhendong Jin, Ken Robinson, Annabelle McIver, and Carroll Morgan. 2005. Development via Refinement in Probabilistic B - Foundation and Case Study. In ZB (Lecture Notes in Computer Science, Vol. 3455). Springer, 355–373.

[28]

Kenneth E. Iverson. 1962. A Programming Language. John Wiley & Sons, Inc., USA. isbn:0471430145

[29]

Sebastian Junges, Joost-Pieter Katoen, Guillermo A. Pérez, and Tobias Winkler. 2021. The complexity of reachability in parametric Markov decision processes. J. Comput. Syst. Sci., 119 (2021), 183–210. https://doi.org/10.1016/J.JCSS.2021.02.006

[30]

Benjamin Lucien Kaminski. 2019. Advanced weakest precondition calculi for probabilistic programs. Ph. D. Dissertation. RWTH Aachen University, Germany.

[31]

Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. 2019. On the hardness of analyzing probabilistic programs. Acta Informatica, 56, 3 (2019), 255–285. https://doi.org/10.1007/S00236-018-0321-1

[32]

Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Federico Olmedo. 2016. Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs. In ESOP (Lecture Notes in Computer Science, Vol. 9632). Springer, 364–389. https://doi.org/10.1007/978-3-662-49498-1_15

[33]

Joost-Pieter Katoen. 2016. The Probabilistic Model Checking Landscape. In LICS. ACM, 31–45. https://doi.org/10.1145/2933575.2934574

[34]

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 SAS (Lecture Notes in Computer Science, Vol. 6337). Springer, 390–406. https://doi.org/10.1007/978-3-642-15769-1_24

[35]

Mark Kattenbelt, Marta Z. Kwiatkowska, Gethin Norman, and David Parker. 2009. Abstraction Refinement for Probabilistic Software. In VMCAI (Lecture Notes in Computer Science, Vol. 5403). Springer, 182–197. https://doi.org/10.1007/978-3-540-93900-9_17

[36]

Mark Kattenbelt, Marta Z. Kwiatkowska, Gethin Norman, and David Parker. 2010. A game-based abstraction-refinement framework for Markov decision processes. Formal Methods Syst. Des., 36, 3 (2010), 246–280. https://doi.org/10.1007/S10703-010-0097-6

[37]

Dexter Kozen. 1983. A Probabilistic PDL. In Proceedings of the 15th Annual ACM Symposium on Theory of Computing, 25-27 April, 1983, Boston, Massachusetts, USA. ACM, 291–297. https://doi.org/10.1145/800061.808758

[38]

Dexter Kozen. 1985. A Probabilistic PDL. J. Comput. Syst. Sci., 30, 2 (1985), 162–178. https://doi.org/10.1016/0022-0000(85)90012-1

[39]

Igor Kozine and Lev V. Utkin. 2002. Interval-Valued Finite Markov Chains. Reliab. Comput., 8, 2 (2002), 97–113. https://doi.org/10.1023/A:1014745904458

[40]

Marta Z. Kwiatkowska, Gethin Norman, and David Parker. 2002. PRISM: Probabilistic Symbolic Model Checker. In Computer Performance Evaluation / TOOLS (Lecture Notes in Computer Science, Vol. 2324). Springer, 200–204. https://doi.org/10.1007/3-540-46029-2_13

[41]

Leslie Lamport. 2002. Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley.

[42]

K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In LPAR (Dakar) (Lecture Notes in Computer Science, Vol. 6355). Springer, 348–370. https://doi.org/10.1007/978-3-642-17511-4_20

[43]

Konstantinos Mamouras. 2016. Synthesis of Strategies Using the Hoare Logic of Angelic and Demonic Nondeterminism. Log. Methods Comput. Sci., 12, 3 (2016), https://doi.org/10.2168/LMCS-12(3:6)2016

[44]

Annabelle McIver and Carroll Morgan. 2005. Abstraction, Refinement and Proof for Probabilistic Systems. Springer. isbn:978-0-387-40115-7 https://doi.org/10.1007/b138392

[45]

Peter Müller, Malte Schwerhoff, and Alexander J. Summers. 2017. Viper: A Verification Infrastructure for Permission-Based Reasoning. In Dependable Software Systems Engineering (NATO Science for Peace and Security Series - D: Information and Communication Security, Vol. 50). IOS Press, 104–125. https://doi.org/10.3233/978-1-61499-810-5-104

[46]

Marcelo Navarro and Federico Olmedo. 2022. Slicing of probabilistic programs based on specifications. Sci. Comput. Program., 220 (2022), 102822. https://doi.org/10.1016/J.SCICO.2022.102822

[47]

Donald Ornstein. 1969. On the existence of stationary optimal strategies. Proc. Amer. Math. Soc., 20, 2 (1969), 563–569.

[48]

David Park. 1969. Fixpoint Induction and Proofs of Program Properties. Machine intelligence, 5 (1969).

[49]

Martin L. Puterman. 1994. Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley. https://doi.org/10.1002/9780470316887

[50]

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.

[51]

Philipp Schröer, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. 2023. A Deductive Verification Infrastructure for Probabilistic Programs. 7, OOPSLA2 (2023), Article 294, oct, 31 pages. https://doi.org/10.1145/3622870

[52]

Martijn van Otterlo and Marco A. Wiering. 2012. Reinforcement Learning and Markov Decision Processes. In Reinforcement Learning (Adaptation, Learning, and Optimization, Vol. 12). Springer, 3–42. https://doi.org/10.1007/978-3-642-27645-3_1

[53]

Wikipedia. 2023. Nim — Wikipedia, The Free Encyclopedia. http://en.wikipedia.org/w/index.php?title=Nim&oldid=1163491825 [Online; accessed 10-July-2023]

Cited By

Xu MFu JJiang HDeng YLi Z(2024)Termination and Universal Termination Problems for Nondeterministic Quantum ProgramsACM Transactions on Software Engineering and Methodology10.1145/369163233:8(1-41)Online publication date: 2-Sep-2024
https://dl.acm.org/doi/10.1145/3691632
Johnsen EKamburjan EPardo RVoogd EWąsowski A(2024)Towards a Proof System for Probabilistic Dynamic LogicPrinciples of Verification: Cycling the Probabilistic Landscape10.1007/978-3-031-75783-9_13(322-338)Online publication date: 13-Nov-2024
https://doi.org/10.1007/978-3-031-75783-9_13
Batz KKaminski BMatheja CWinkler T(2024)J-P: MDP. FP. PPPrinciples of Verification: Cycling the Probabilistic Landscape10.1007/978-3-031-75783-9_11(255-302)Online publication date: 13-Nov-2024
https://doi.org/10.1007/978-3-031-75783-9_11
Show More Cited By

Index Terms

Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs
1. Theory of computation

Recommendations

A Deductive Verification Infrastructure for Probabilistic Programs

This paper presents a quantitative program verification infrastructure for discrete probabilistic programs. Our infrastructure can be viewed as the probabilistic analogue of Boogie: its central components are an intermediate verification language (...
Lower Bounds for Possibly Divergent Probabilistic Programs

We present a new proof rule for verifying lower bounds on quantities of probabilistic programs. Our proof rule is not confined to almost-surely terminating programs -- as is the case for existing rules -- and can be used to establish non-trivial lower ...
Stochastic invariants for probabilistic termination
POPL '17

Termination is one of the basic liveness properties, and we study the termination problem for probabilistic programs with real-valued variables. Previous works focused on the qualitative problem that asks whether an input program terminates with ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 8, Issue POPL

January 2024

2820 pages

EISSN:2475-1421

DOI:10.1145/3554315

Editor:
Michael Hicks
Amazon, USA

Issue’s Table of Contents

Copyright © 2024 Owner/Author.

This work is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 05 January 2024

Published in PACMPL Volume 8, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
449
Total Downloads

Downloads (Last 12 months)449
Downloads (Last 6 weeks)57

Reflects downloads up to 12 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Xu MFu JJiang HDeng YLi Z(2024)Termination and Universal Termination Problems for Nondeterministic Quantum ProgramsACM Transactions on Software Engineering and Methodology10.1145/369163233:8(1-41)Online publication date: 2-Sep-2024
https://dl.acm.org/doi/10.1145/3691632
Johnsen EKamburjan EPardo RVoogd EWąsowski A(2024)Towards a Proof System for Probabilistic Dynamic LogicPrinciples of Verification: Cycling the Probabilistic Landscape10.1007/978-3-031-75783-9_13(322-338)Online publication date: 13-Nov-2024
https://doi.org/10.1007/978-3-031-75783-9_13
Batz KKaminski BMatheja CWinkler T(2024)J-P: MDP. FP. PPPrinciples of Verification: Cycling the Probabilistic Landscape10.1007/978-3-031-75783-9_11(255-302)Online publication date: 13-Nov-2024
https://doi.org/10.1007/978-3-031-75783-9_11
Abate AGiacobbe MRoy DSchnitzer Y(2024)Model Checking and Strategy Synthesis with Abstractions and CertificatesPrinciples of Verification: Cycling the Probabilistic Landscape10.1007/978-3-031-75775-4_16(360-391)Online publication date: 13-Nov-2024
https://doi.org/10.1007/978-3-031-75775-4_16
Abate AGiacobbe MRoy D(2024)Stochastic Omega-Regular Verification and Control with SupermartingalesComputer Aided Verification10.1007/978-3-031-65633-0_18(395-419)Online publication date: 26-Jul-2024
https://doi.org/10.1007/978-3-031-65633-0_18

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents