research-article

Open access

Aiming low is harder: induction for lower bounds in probabilistic program verification

Authors:

Benjamin Lucien Kaminski,

Joost-Pieter KatoenAuthors Info & Claims

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

Article No.: 37, Pages 1 - 28

https://doi.org/10.1145/3371105

Published: 20 December 2019 Publication History

Abstract

We present a new inductive rule for verifying lower bounds on expected values of random variables after execution of probabilistic loops as well as on their expected runtimes. Our rule is simple in the sense that loop body semantics need to be applied only finitely often in order to verify that the candidates are indeed lower bounds. In particular, it is not necessary to find the limit of a sequence as in many previous rules.

Supplementary Material

WEBM File (a37-hark.webm)

Download
86.77 MB

References

[1]

Sheshansh Agrawal, Krishnendu Chatterjee, and Petr Novotný. 2018. Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs. PACMPL 2, POPL (2018), 34:1–34:32.

Digital Library

[2]

Philippe Audebaud and Christine Paulin-Mohring. 2009. Proofs of Randomized Algorithms in Coq. Science of Computer Programming 74, 8 (2009), 568–589.

Digital Library

[3]

Ralph-Johan Back and Joakim von Wright. 1998. Refinement Calculus - A Systematic Introduction. Springer.

[4]

Andrei Baranga. 1991. The Contraction Principle as a Particular Case of Kleene’s Fixed Point Theorem. Discrete Mathematics 98, 1 (1991), 75–79.

Digital Library

[5]

Gilles Barthe, Thomas Espitau, Luis María Ferrer Fioriti, and Justin Hsu. 2016. Synthesizing Probabilistic Invariants via Doob’s Decomposition. In Proc. of the International Conference on Computer–Aided Verification (CAV) (Lecture Notes in Computer Science), Vol. 9779. Springer, 43–61.

[6]

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. PACMPL 3, POPL (2019), 34:1–34:29.

[7]

Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. 2018. How Long, O Bayesian Network, will I Sample Thee? - A Program Analysis Perspective on Expected Sampling Times. In Proc. of the European Symposium on Programming Languages and Systems (ESOP) (Lecture Notes in Computer Science), Vol. 10801. Springer, 186–213.

[8]

Heinz Bauer. 1971. Probability Theory and Elements of Measure Theory (first english ed.). Holt, Rinehart and Winston, Inc., New York.

[9]

Aleksandar Chakarov and Sriram Sankaranarayanan. 2013. Probabilistic Program Analysis with Martingales. In Proc. of the International Conference on Computer–Aided Verification (CAV) (Lecture Notes in Computer Science), Vol. 8044. Springer, 511–526.

[10]

Aleksandar Chakarov and Sriram Sankaranarayanan. 2014. Expectation Invariants for Probabilistic Program Loops as Fixed Points. In Proc. of the Static Analysis Symposium (SAS) (Lecture Notes in Computer Science), Vol. 8723. Springer, 85–100.

[11]

Krishnendu Chatterjee, Hongfei Fu, Petr Novotný, and Rouzbeh Hasheminezhad. 2016. Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs. In Proc. of the Symposium on Principles of Programming Languages (POPL). ACM, 327–342.

Digital Library

[12]

Krishnendu Chatterjee, Petr Novotný, and Dorde Zikelic. 2017. Stochastic Invariants for Probabilistic Termination. In Proc. of the Symposium on Principles of Programming Languages (POPL). ACM, 145–160.

Digital Library

[13]

Yu-Fang Chen, Chih-Duo Hong, Bow-Yaw Wang, and Lijun Zhang. 2015. Counterexample–Guided Polynomial Loop Invariant Generation by Lagrange Interpolation. In Proc. of the International Conference on Computer–Aided Verification (CAV) (Lecture Notes in Computer Science), Vol. 9206. Springer, 658–674.

[14]

David Cock. 2014. pGCL for Isabelle. Archive of Formal Proofs (2014).

[15]

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

Digital Library

[16]

Edsger Wybe Dijkstra. 1976. A Discipline of Programming. Prentice–Hall.

[17]

William Feller. 1971. An Introduction to Probability Theory and its Applications. Vol. II. John Wiley & Sons.

[18]

Yijun Feng, Lijun Zhang, David Nicolaas Jansen, Naijun Zhan, and Bican Xia. 2017. Finding Polynomial Loop Invariants for Probabilistic Programs. In Proc. of the International Symposium on Automated Technology for Verification and Analysis (ATVA) (Lecture Notes in Computer Science), Vol. 10482. Springer, 400–416.

[19]

Luis María Ferrer Fioriti and Holger Hermanns. 2015. Probabilistic Termination: Soundness, Completeness, and Compositionality. In Proc. of the Symposium on Principles of Programming Languages (POPL). ACM, 489–501.

Digital Library

[20]

Florian Frohn, Matthias Naaf, Jera Hensel, Marc Brockschmidt, and Jürgen Giesl. 2016. Lower Runtime Bounds for Integer Programs. In Proc. of the International Joint Conference on Automated Reasoning (IJCAR) (Lecture Notes in Computer Science), Vol. 9706. Springer, 550–567.

Digital Library

[21]

Hongfei Fu and Krishnendu Chatterjee. 2019. Termination of Nondeterministic Probabilistic Programs. In Proc. of the International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI) (Lecture Notes in Computer Science), Vol. 11388. Springer, 468–490.

[22]

Andrew D. Gordon, Thomas A. Henzinger, Aditya Vithal Nori, and Sriram K. Rajamani. 2014. Probabilistic Programming. In Proc. of Future of Software Engineering (FOSE). ACM, 167–181.

[23]

Geoffrey Grimmett and David Stirzaker. 2001. Probability and Random Processes. Oxford University Press, Oxford; New York.

[24]

Marcel Hark, Benjamin Lucien Kaminski, Jürgen Giesl, and Joost-Pieter Katoen. 2019. Aiming Low Is Harder - Inductive Proof Rules for Lower Bounds on Weakest Preexpectations in Probabilistic Program Verification. CoRR abs/1904.01117 (2019). arXiv: 1904.01117

[25]

Eric Charles Roy Hehner. 2011. A Probability Perspective. Formal Aspects of Computing 23, 4 (2011), 391–419.

[26]

Wataru Hino, Hiroki Kobayashi, Ichiro Hasuo, and Bart Jacobs. 2016. Healthiness from Duality. In Proc. of the Annual Symposium on Logic in Computer Science (LICS). ACM, 682–691.

Digital Library

[27]

Mingzhang Huang, Hongfei Fu, and Krishnendu Chatterjee. 2018. New Approaches for Almost–Sure Termination of Probabilistic Programs (Lecture Notes in Computer Science), Vol. 11275. Springer, 181–201.

[28]

Jacek Jachymski, Leslaw Gajek, and Piotr Pokarowski. 2000. The Tarski–Kantorovitch Principle and the Theory of Iterated Function Systems. Bulletin of the Australian Mathematical Society 61, 2 (2000), 247–261.

[29]

Nils Jansen, Christian Dehnert, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Lukas Westhofen. 2016. Bounded Model Checking for Probabilistic Programs. In Proc. of the International Symposium on Automated Technology for Verification and Analysis (ATVA) (Lecture Notes in Computer Science), Vol. 9938. Springer, 68–85.

[30]

Claire Jones. 1990. Probabilistic Non–Determinism. Ph.D. Dissertation. University of Edinburgh, UK.

[31]

Benjamin Lucien Kaminski. 2019. Advanced Weakest Precondition Calculi for Probabilistic Programs. Ph.D. Dissertation. RWTH Aachen University, Germany. http://publications.rwth-aachen.de/record/755408/files/755408.pdf

[32]

Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. 2019. On the Hardness of Analyzing Probabilistic Programs. Acta Inf. 56, 3 (2019), 255–285.

Digital Library

[33]

Benjamin Lucien Kaminski and Joost-Pieter Katoen. 2017. A Weakest Pre–expectation Semantics for Mixed–sign Expectations. In Proc. of the Annual Symposium on Logic in Computer Science (LICS). IEEE Computer Society, 1–12.

[34]

Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Federico Olmedo. 2016. Weakest Precondition Reasoning for Expected Run–Times of Probabilistic Programs. In Proc. of the European Symposium on Programming Languages and Systems (ESOP) (Lecture Notes in Computer Science), Vol. 9632. Springer, 364–389.

Digital Library

[35]

Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Federico Olmedo. 2018. Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms. Journal of the ACM 65 (2018).

[36]

Joost-Pieter Katoen, Annabelle McIver, Larissa Meinicke, and Carroll Morgan. 2010. Linear-Invariant Generation for Probabilistic Programs: Automated Support for Proof–Based Methods. In Proc. of the Static Analysis Symposium (SAS) (Lecture Notes in Computer Science), Vol. 6337. Springer, 390–406.

[37]

Klaus Keimel. 2015. Healthiness Conditions for Predicate Transformers. Electr. Notes Theor. Comput. Sci. 319 (2015), 255–270.

Digital Library

[38]

Naoki Kobayashi, Ugo Dal Lago, and Charles Grellois. 2018. On the Termination Problem for Probabilistic Higher-Order Recursive Programs. CoRR abs/1811.02133 (2018). arXiv: 1811.02133

[39]

Dexter Kozen. 1983. A Probabilistic PDL. In Proc. of the Annual Symposium on Theory of Computing (STOC). 291–297.

Digital Library

[40]

Dexter Kozen. 1985. A Probabilistic PDL. J. Comput. System Sci. 30, 2 (1985), 162–178.

[41]

Jean-Louis Lassez, V. L. Nguyen, and Liz Sonenberg. 1982. Fixed Point Theorems and Semantics: A Folk Tale. Inform. Process. Lett. 14, 3 (1982), 112–116.

[42]

Annabelle McIver and Carroll Morgan. 2001. Partial Correctness for Probabilistic Demonic Programs. Theoretical Computer Science 266, 1-2 (2001), 513–541.

Digital Library

[43]

Annabelle McIver and Carroll Morgan. 2005. Abstraction, Refinement and Proof for Probabilistic Systems. Springer.

Digital Library

[44]

David Monniaux. 2005. Abstract Interpretation of Programs as Markov Decision Processes. Science of Computer Programming 58, 1–2 (2005), 179–205.

Digital Library

[45]

Carroll Morgan. 1996. Proof Rules for Probabilistic Loops. In Proc. of BCS–FACS 7th Refinement Workshop.

[46]

Carroll Morgan and Annabelle McIver. 1999. An Expectation–Transformer Model for Probabilistic Temporal Logic. Logic Journal of the Interest Group in Pure and Applied Logics 7, 6 (1999), 779–804.

[47]

Carroll Morgan, Annabelle McIver, and Karen Seidel. 1996. Probabilistic Predicate Transformers. ACM Trans. on Programming Languages and Systems 18, 3 (1996), 325–353.

Digital Library

[48]

Rajeev Motwani and Prabhakar Raghavan. 1995. Randomized Algorithms. Cambridge University Press.

Digital Library

[49]

Van Chan Ngo, Quentin Carbonneaux, and Jan Hoffmann. 2018. Bounded Expectations: Resource Analysis for Probabilistic Programs. In Proc. of the Conference on Programming Language Design and Implementation (PLDI). ACM, 496–512.

Digital Library

[50]

Federico Olmedo, Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Annabelle McIver. 2018. Conditioning in Probabilistic Programming. ACM Trans. on Programming Languages and Systems 40, 1 (2018), 4:1–4:50.

Digital Library

[51]

Federico Olmedo, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. 2016. Reasoning about Recursive Probabilistic Programs. In Proc. of the Annual Symposium on Logic in Computer Science (LICS). ACM, 672–681.

Digital Library

[52]

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

[53]

George Pólya. 1930. Eine Wahrscheinlichkeitsaufgabe in der Kundenwerbung. Zeitschrift für Angewandte Mathematik und Mechanik 10, 1 (1930), 96–97.

[54]

Moshe Ya’akov Vardi. 1985. Automatic Verification of Probabilistic Concurrent Finite–State Programs. In Proc. of the Annual Symposium on Foundations of Computer Science (FOCS). IEEE Computer Society, 327–338.

Digital Library

[55]

Peixin Wang, Hongfei Fu, Amir Kafshdar Goharshady, Krishnendu Chatterjee, Xudong Qin, and Wenjun Shi. 2019. Cost Analysis of Nondeterministic Probabilistic Programs. In Proc. of the Conference on Programming Language Design and Implementation (PLDI). ACM, 204–220.

Digital Library

Cited By

Avanzini MBarthe GDavoli DGrégoire B(2025)A Quantitative Probabilistic Relational Hoare LogicProceedings of the ACM on Programming Languages10.1145/37048769:POPL(1167-1195)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704876
Haselwarter PLi Kde Medeiros MGregersen SAguirre ATassarotti JBirkedal L(2024)Tachis: Higher-Order Separation Logic with Credits for Expected CostsProceedings of the ACM on Programming Languages10.1145/36897538:OOPSLA2(1189-1218)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689753
Zhang LZilberstein NKaminski BSilva A(2024)Quantitative Weakest Hyper Pre: Unifying Correctness and Incorrectness Hyperproperties via Predicate TransformersProceedings of the ACM on Programming Languages10.1145/36897408:OOPSLA2(817-845)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689740
Show More Cited By

Index Terms

Aiming low is harder: induction for lower bounds in probabilistic program verification
1. Mathematics of computing
  1. Probability and statistics
    1. Probabilistic algorithms
    2. Stochastic processes
      1. Markov processes
2. Theory of computation
  1. Semantics and reasoning
    1. Program semantics
      1. Denotational semantics

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 (...
Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning

We study a syntax for specifying quantitative assertions—functions mapping program states to numbers—for probabilistic program verification. We prove that our syntax is expressive in the following sense: Given any probabilistic program C, if a function f ...
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 ...

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 4, Issue POPL

January 2020

1984 pages

EISSN:2475-1421

DOI:10.1145/3377388

Issue’s Table of Contents

Copyright © 2019 Owner/Author.

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

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 20 December 2019

Published in PACMPL Volume 4, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Deutsche Forschungsgemeinschaft
European Research Council

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

29
Total Citations
View Citations
978
Total Downloads

Downloads (Last 12 months)187
Downloads (Last 6 weeks)16

Reflects downloads up to 05 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Avanzini MBarthe GDavoli DGrégoire B(2025)A Quantitative Probabilistic Relational Hoare LogicProceedings of the ACM on Programming Languages10.1145/37048769:POPL(1167-1195)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704876
Haselwarter PLi Kde Medeiros MGregersen SAguirre ATassarotti JBirkedal L(2024)Tachis: Higher-Order Separation Logic with Credits for Expected CostsProceedings of the ACM on Programming Languages10.1145/36897538:OOPSLA2(1189-1218)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689753
Zhang LZilberstein NKaminski BSilva A(2024)Quantitative Weakest Hyper Pre: Unifying Correctness and Incorrectness Hyperproperties via Predicate TransformersProceedings of the ACM on Programming Languages10.1145/36897408:OOPSLA2(817-845)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689740
Kura SUnno H(2024)Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type SystemProceedings of the ACM on Programming Languages10.1145/36746628:ICFP(973-1002)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674662
Chatterjee KGoharshady ENovotný PŽikelić Đ(2024)Equivalence and Similarity Refutation for Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/36564628:PLDI(2098-2122)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656462
Klinkenberg LBlumenthal CChen MHaase DKatoen J(2024)Exact Bayesian Inference for Loopy Probabilistic Programs using Generating FunctionsProceedings of the ACM on Programming Languages10.1145/36498448:OOPSLA1(923-953)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649844
Batz KBiskup TKatoen JWinkler T(2024)Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/36329358:POPL(2792-2820)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632935
Bao JTrivedi NPathak DHsu JRoy S(2024)Data-driven invariant learning for probabilistic programsFormal Methods in System Design10.1007/s10703-024-00466-xOnline publication date: 3-Dec-2024
https://doi.org/10.1007/s10703-024-00466-x
Moosbrugger MMüllner JBartocci EKovács L(2024)Polar: An Algebraic Analyzer for (Probabilistic) LoopsPrinciples of Verification: Cycling the Probabilistic Landscape10.1007/978-3-031-75783-9_8(179-200)Online publication date: 13-Nov-2024
https://doi.org/10.1007/978-3-031-75783-9_8
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

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

Figures

Tables

Media

View Issue’s Table of Contents