[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ skip to main content
research-article
Open access

Ranking and Repulsing Supermartingales for Reachability in Randomized Programs

Published: 08 June 2021 Publication History

Abstract

Computing reachability probabilities is a fundamental problem in the analysis of randomized programs. This article aims at a comprehensive and comparative account of various martingale-based methods 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—a classic topic in computer science—in 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.

References

[1]
Alessandro Abate, Joost-Pieter Katoen, John Lygeros, and Maria Prandini. 2010. Approximate model checking of stochastic hybrid systems. Eur. J. Cont. 16, 6 (2010), 624–641.
[2]
Sheshansh Agrawal, Krishnendu Chatterjee, and Petr Novotný. 2018. Lexicographic ranking supermartingales: An efficient approach to termination of probabilistic programs. Proc. ACM Prog. Lang. 2, POPL (2018), 34:1–34:32.
[3]
Christophe Alias, Alain Darte, Paul Feautrier, and Laure Gonnord. 2010. Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In Proceedings of the 17th International Static Analysis Symposium, (SAS’10) (Lecture Notes in Computer Science), Radhia Cousot and Matthieu Martel (Eds.), Vol. 6337. Springer, 117–133.
[4]
Krzysztof R. Apt and Gordon D. Plotkin. 1986. Countable nondeterminism and random assignment. J. ACM 33, 4 (1986), 724–767.
[5]
André Arnold and Damian Niwiński. 2001. Rudiments of -Calculus. Elsevier.
[6]
Martin Avanzini, Ugo Dal Lago, and Akihisa Yamada. 2018. On probabilistic term rewriting. In Proceedings of the International Symposium on Functional and Logic Programming (FLOPS’18) (Lecture Notes in Computer Science), John P. Gallagher and Martin Sulzmann (Eds.), Vol. 10818. Springer, 132–148.
[7]
Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. The MIT Press.
[8]
Dimitri P. Bertsekas and Steven E. Shreve. 2007. Stochastic Optimal Control: The Discrete-Time Case. Athena Scientific.
[9]
Rastislav Bodík and Rupak Majumdar (Eds.). 2016. In Proceedings of the ACM SIGPLAN Symposium on Principles of Programming Languages. ACM.
[10]
Aleksandar Chakarov and Sriram Sankaranarayanan. 2013. Probabilistic program analysis with martingales. In Proceedings of the International Conference on Computer Aided Verification (LNCS), Natasha Sharygina and Helmut Veith (Eds.), Vol. 8044. Springer, 511–526.
[11]
Aleksandar Chakarov, Yuen-Lam Voronin, and Sriram Sankaranarayanan. 2016. Deductive proofs of almost sure persistence and recurrence properties. In Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, (TACAS’16) (LNCS), Marsha Chechik and Jean-François Raskin (Eds.), Vol. 9636. Springer, 260–279.
[12]
Krishnendu Chatterjee and Hongfei Fu. 2017. Termination of nondeterministic recursive probabilistic programs. CoRR abs/1701.02944 (2017).
[13]
Krishnendu Chatterjee, Hongfei Fu, and Amir Kafshdar Goharshady. 2016. Termination analysis of probabilistic programs through Positivstellensatz’s. In Proceedings of the International Conference on Computer Aided Verification (LNCS), Swarat Chaudhuri and Azadeh Farzan (Eds.), Vol. 9779. Springer, 3–22.
[14]
Krishnendu Chatterjee, Hongfei Fu, Petr Novotný, and Rouzbeh Hasheminezhad. 2016. Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. In Proceedings of the ACM SIGPLAN Symposium on Principles of Programming Languages.327–342.
[15]
Krishnendu Chatterjee, Petr Novotný, and Dorde Zikelic. 2017. Stochastic invariants for probabilistic termination. In Proceedings of the ACM SIGPLAN Symposium on Principles of Programming Languages (POPL’17), Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 145–160.
[16]
Radhia Cousot and Patrick Cousot. 1979. Constructive versions of Tarski’s fixed point theorems. Pacific J. Math. 82, 1 (1979), 43–57.
[17]
Luis María Ferrer Fioriti and Holger Hermanns. 2015. Probabilistic termination: Soundness, completeness, and compositionality. In Proceedings of the 42nd SIGPLAN-SIGACT Symposium on Principles of Programming Languages, (POPL’15), Sriram K. Rajamani and David Walker (Eds.). ACM, 489–501.
[18]
A. Makhorin. 2008. GLPK–GNU Linear Programming Kit. http://www.gnu.org/software/glpk/.
[19]
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’14), James D. Herbsleb and Matthew B. Dwyer (Eds.). ACM, 167–181.
[20]
Ichiro Hasuo, Shunsuke Shimizu, and Corina Cîrstea. 2016. Lattice-theoretic progress measures and coalgebraic model checking. In Proceedings of the ACM SIGPLAN Symposium on Principles of Programming Languages. 718–732.
[21]
Roger A. Horn and Charles R. Johnson. 2012. Matrix Analysis (2nd ed.). Cambridge University Press, New York, NY.
[22]
Marcin Jurdzinski. 2000. Small progress measures for solving parity games. In Proceedings of the International Symposium on Theoretical Aspects of Computer Science (STACS’00) (LNCS), Horst Reichel and Sophie Tison (Eds.), Vol. 1770. Springer, 290–301.
[23]
Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Federico Olmedo. 2016. Weakest precondition reasoning for expected run-times of probabilistic programs. In Proceedings of the 25th European Symposium on Programming Languages and Systems, (ESOP’16), Held as Part of the European Joint Conferences on Theory and Practice of Software, (ETAPS’16) (Lecture Notes in Computer Science), Peter Thiemann (Ed.), Vol. 9632. Springer, 364–389.
[24]
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’10). 390–406.
[25]
Dexter Kozen. 1985. A probabilistic PDL. J. Comput. Syst. Sci. 30, 2 (1985), 162–178.
[26]
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’19), Held as Part of the European Joint Conferences on Theory and Practice of Software, (ETAPS’19) (Lecture Notes in Computer Science), Tomás Vojnar and Lijun Zhang (Eds.), Vol. 11428. Springer, 135–153.
[27]
Annabelle McIver and Carroll Morgan. 2004. Abstraction, Refinement and Proof for Probabilistic Systems (Monographs in Computer Science). SpringerVerlag.
[28]
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’04) (LNCS), Ana Cavalcanti, Augusto Sampaio, and Jim Woodcock (Eds.), Vol. 3167. Springer, 123–155.
[29]
Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, and Joost-Pieter Katoen. 2018. A new proof rule for almost-sure termination. Proc. ACM Prog. Lang. 2, POPL (2018), 33:1–33:28.
[30]
Frederick Mosteller. 2012. Fifty Challenging Problems in Probability with Solutions. Dover Publications.
[31]
Arkadi Nemirovski and Cornelis Roos. 2008. Motzkin transposition theorem. Encyclopedia of Optimization (2nd edition), C. A. Floudas and P. M. Pardalos (Eds.). Springer, 235–2348. https://doi.org/10.1007/978-0-387-74759-0_405.
[32]
Van Chan Ngo, Quentin Carbonneaux, and Jan Hoffmann. 2018. Bounded expectations: Resource analysis for probabilistic programs. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, (PLDI’18), Jeffrey S. Foster and Dan Grossman (Eds.). ACM, 496–512.
[33]
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–934.
[34]
Konrad Schmüdgen. 1991. The K-moment problem for compact semi-algebraic sets. Math. Ann. 289, 1 (01 Mar. 1991), 203–206.
[35]
Alexander Schrijver. 1998. Theory of Linear and Integer Programming. Wiley.
[36]
K. C. Toh, M. J. Todd, and R. H. Tutuncu, SDPT3–a Matlab software package for semidefinite programming. Optimization Methods and Software 11 (1999), 545–581.
[37]
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.
[38]
Jacob Steinhardt and Russ Tedrake. 2012. Finite-time regional verification of stochastic non-linear systems. Int. J. Robot. Res. 31, 7 (2012), 901–923.
[39]
Toru Takisaka, Yuichiro Oyabu, Natsuki Urabe, and Ichiro Hasuo. 2018. Ranking and repulsing supermartingales for reachability in probabilistic programs. In Proceedings of the 16th International Symposium on Automated Technology for Verification and Analysis, (ATVA’18) (Lecture Notes in Computer Science), Shuvendu K. Lahiri and Chao Wang (Eds.), Vol. 11138. Springer, 476–493.
[40]
Alfred Tarski. 1951. A Decision Method for Elementary Algebra and Geometry. University of California Press, Berkeley.
[41]
Natsuki Urabe, Masaki Hara, and Ichiro Hasuo. 2017. Categorical liveness checking by corecursive algebras. In Proceedings of the ACM-IEEE Symposium on Logic in Computer Science (LICS’17). IEEE Computer Society, 1–12.
[42]
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–266.

Cited By

View all
  • (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
  • (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
  • (2024)Quantitative Bounds on Resource Usage of Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/36498248:OOPSLA1(362-391)Online publication date: 29-Apr-2024
  • Show More Cited By

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems
ACM Transactions on Programming Languages and Systems  Volume 43, Issue 2
June 2021
197 pages
ISSN:0164-0925
EISSN:1558-4593
DOI:10.1145/3470134
Issue’s Table of Contents
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: 08 June 2021
Accepted: 01 February 2021
Revised: 01 January 2021
Received: 01 May 2019
Published in TOPLAS Volume 43, Issue 2

Check for updates

Author Tags

  1. Randomized program
  2. fixed point
  3. martingale
  4. reachability

Qualifiers

  • Research-article
  • Research
  • Refereed

Funding Sources

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)239
  • Downloads (Last 6 weeks)29
Reflects downloads up to 20 Dec 2024

Other Metrics

Citations

Cited By

View all
  • (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
  • (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
  • (2024)Quantitative Bounds on Resource Usage of Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/36498248:OOPSLA1(362-391)Online publication date: 29-Apr-2024
  • (2024)Positive Almost-Sure Termination: Complexity and Proof RulesProceedings of the ACM on Programming Languages10.1145/36328798:POPL(1089-1117)Online publication date: 5-Jan-2024
  • (2024)A Unified Framework for Quantitative Analysis of Probabilistic ProgramsPrinciples of Verification: Cycling the Probabilistic Landscape10.1007/978-3-031-75783-9_10(230-254)Online publication date: 13-Nov-2024
  • (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
  • (2024)Sound and Complete Witnesses for Template-Based Verification of LTL Properties on Polynomial ProgramsFormal Methods10.1007/978-3-031-71162-6_31(600-619)Online publication date: 11-Sep-2024
  • (2024)Lexicographic Ranking Supermartingales with Lazy Lower BoundsComputer Aided Verification10.1007/978-3-031-65633-0_19(420-442)Online publication date: 24-Jul-2024
  • (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
  • (2024)Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled SystemsComputer Aided Verification10.1007/978-3-031-65630-9_20(401-426)Online publication date: 25-Jul-2024
  • Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

HTML Format

View this article in HTML Format.

HTML Format

Login options

Full Access

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media