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

research-article

Open access

Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs

Authors:

Sheshansh Agrawal,

Krishnendu Chatterjee,

Petr NovotnýAuthors Info & Claims

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

Article No.: 34, Pages 1 - 32

https://doi.org/10.1145/3158122

Published: 27 December 2017 Publication History

Abstract

Probabilistic programs extend classical imperative programs with real-valued random variables and random branching. The most basic liveness property for such programs is the termination property. The qualitative (aka almost-sure) termination problem asks whether a given program program terminates with probability 1. While ranking functions provide a sound and complete method for non-probabilistic programs, the extension of them to probabilistic programs is achieved via ranking supermartingales (RSMs). Although deep theoretical results have been established about RSMs, their application to probabilistic programs with nondeterminism has been limited only to programs of restricted control-flow structure. For non-probabilistic programs, lexicographic ranking functions provide a compositional and practical approach for termination analysis of real-world programs. In this work we introduce lexicographic RSMs and show that they present a sound method for almost-sure termination of probabilistic programs with nondeterminism. We show that lexicographic RSMs provide a tool for compositional reasoning about almost-sure termination, and for probabilistic programs with linear arithmetic they can be synthesized efficiently (in polynomial time). We also show that with additional restrictions even asymptotic bounds on expected termination time can be obtained through lexicographic RSMs. Finally, we present experimental results on benchmarks adapted from previous work to demonstrate the effectiveness of our approach.

Supplementary Material

WEBM File (lexicographicranking.webm)

Download
101.26 MB

References

[1]

2010. IBM ILOG CPLEX Optimizer. http://www-01.ibm.com/software/integration/optimization/cplex-optimizer/.

[2]

Sheshansh Agrawal, Krishnendu Chatterjee, and Petr Novotný. 2017. Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs. CoRR abs/1709.04037 (2017). http://arxiv.org/abs/1709.04037

[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 Conference on Static Analysis (SAS’10). Springer-Verlag, Berlin, Heidelberg, 117–133. http://dl.acm.org/citation.cfm?id=1882094.1882102

[4]

R.B. Ash and C. Doléans-Dade. 2000. Probability and Measure Theory. Harcourt/Academic Press.

[5]

Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. The MIT Press, Cambridge, Massachusetts. 984 pages.

Digital Library

[6]

Gilles Barthe, Thomas Espitau, Luis María Ferrer Fioriti, and Justin Hsu. 2016a. Synthesizing Probabilistic Invariants via Doob’s Decomposition. In Computer Aided Verification: 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I, Swarat Chaudhuri and Azadeh Farzan (Eds.). Springer International Publishing, 43–61.

[7]

Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2016b. Proving Differential Privacy via Probabilistic Couplings. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS ’16). ACM, New York, NY, USA, 749–758.

Digital Library

[8]

Gilles Barthe, Marco Gaboardi, Justin Hsu, and Benjamin Pierce. 2016c. Programming Language Techniques for Differential Privacy. ACM SIGLOG News 3, 1 (Feb. 2016), 34–53.

Digital Library

[9]

Amir M. Ben-Amram and Samir Genaim. 2013. On the Linear Ranking Problem for Integer Linear-constraint Loops. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’13). ACM, New York, NY, USA, 51–62.

Digital Library

[10]

Amir M. Ben-Amram and Samir Genaim. 2015. Complexity of Bradley-Manna-Sipma Lexicographic Ranking Functions. In Computer Aided Verification: 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II, Daniel Kroening and Corina S. Păsăreanu (Eds.). Springer International Publishing, 304–321.

[11]

P. Billingsley. 1995. Probability and Measure (3rd ed.). Wiley.

[12]

Olivier Bournez and Florent Garnier. 2005. Proving Positive Almost-Sure Termination. In RTA. 323–337.

Digital Library

[13]

Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. 2005a. Linear Ranking with Reachability. In Computer Aided Verification, 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings (Lecture Notes in Computer Science), Kousha Etessami and Sriram K. Rajamani (Eds.), Vol. 3576. Springer, 491–504.

Digital Library

[14]

Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. 2005b. The Polyranking Principle. In ICALP. 1349–1361.

Digital Library

[15]

Marc Brockschmidt, Byron Cook, Samin Ishtiaq, Heidy Khlaaf, and Nir Piterman. 2016. T2: Temporal Property Verification. In Tools and Algorithms for the Construction and Analysis of Systems: 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, Marsha Chechik and Jean-François Raskin (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 387–393.

Digital Library

[16]

Aleksandar Chakarov and Sriram Sankaranarayanan. 2013. Probabilistic Program Analysis with Martingales. In Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings (Lecture Notes in Computer Science), Natasha Sharygina and Helmut Veith (Eds.), Vol. 8044. Springer, 511–526.

Digital Library

[17]

Aleksandar Chakarov, Yuen-Lam Voronin, and Sriram Sankaranarayanan. 2016. Deductive Proofs of Almost Sure Persistence and Recurrence Properties. In Tools and Algorithms for the Construction and Analysis of Systems: 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, Marsha Chechik and Jean-François Raskin (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 260–279.

Digital Library

[18]

Krishnendu Chatterjee and Hongfei Fu. 2017. Termination of Nondeterministic Recursive Probabilistic Programs. CoRR abs/1701.02944 (2017). http://arxiv.org/abs/1701.02944

[19]

Krishnendu Chatterjee, Hongfei Fu, and Amir Kafshdar Goharshady. 2016a. Termination Analysis of Probabilistic Programs Through Positivstellensatz’s. In CAV. 3–22.

[20]

Krishnendu Chatterjee, Hongfei Fu, Petr Novotný, and Rouzbeh Hasheminezhad. 2016b. Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, Rastislav Bodík and Rupak Majumdar (Eds.). ACM, 327–342.

Digital Library

[21]

Krishnendu Chatterjee, Petr Novotný, and Djordje Žikelić. 2017. Stochastic Invariants for Probabilistic Termination. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017). ACM, New York, NY, USA, 145–160.

Digital Library

[22]

Aziem Chawdhary, Byron Cook, Sumit Gulwani, Mooly Sagiv, and Hongseok Yang. 2008. Ranking Abstractions. In Programming Languages and Systems: 17th European Symposium on Programming, ESOP 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, Sophia Drossopoulou (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 148–162.

[23]

Michael Colón and Henny Sipma. 2001. Synthesis of Linear Ranking Functions. In Tools and Algorithms for the Construction and Analysis of Systems, 7th International Conference, TACAS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2-6, 2001, Proceedings (Lecture Notes in Computer Science), Tiziana Margaria and Wang Yi (Eds.), Vol. 2031. Springer, 67–81.

[24]

Byron Cook, Andreas Podelski, and Andrey Rybalchenko. 2006. Termination Proofs for Systems Code. In Proceedings of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’06). ACM, New York, NY, USA, 415–426.

Digital Library

[25]

Byron Cook, Andreas Podelski, and Andrey Rybalchenko. 2011. Proving program termination. Commun. ACM 54, 5 (2011), 88–98.

Digital Library

[26]

Byron Cook, Abigail See, and Florian Zuleger. 2013. Ramsey vs. Lexicographic Termination Proving. In Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’13). Springer-Verlag, Berlin, Heidelberg, 47–61.

Digital Library

[27]

Patrick Cousot and Radhia Cousot. 1977. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977, Robert M. Graham, Michael A. Harrison, and Ravi Sethi (Eds.). ACM, 238–252.

Digital Library

[28]

Devdatt Dubhashi and Alessandro Panconesi. 2009. Concentration of Measure for the Analysis of Randomized Algorithms (1st ed.). Cambridge University Press, New York, NY, USA.

[29]

Javier Esparza, Andreas Gaiser, and Stefan Kiefer. 2012. Proving Termination of Probabilistic Programs Using Patterns. In CAV. 123–138.

Digital Library

[30]

Paul Feautrier and Laure Gonnord. 2010. Accelerated Invariant Generation for C Programs with Aspic and C2fsm. Electronic Notes in Theoretical Computer Science 267, 2 (2010), 3 – 13.

Digital Library

[31]

Yishai A. Feldman. 1984. A decidable propositional dynamic logic with explicit probabilities. Information and Control 63, 1 (1984), 11–38.

Digital Library

[32]

Yishai A Feldman and David Harel. 1982. A probabilistic dynamic logic. In Proceedings of the fourteenth annual ACM Symposium on Theory of computing. ACM, 181–195.

Digital Library

[33]

Luis María Ferrer Fioriti and Holger Hermanns. 2015. Probabilistic Termination: Soundness, Completeness, and Compositionality. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, Sriram K. Rajamani and David Walker (Eds.). ACM, 489–501.

Digital Library

[34]

Robert W. Floyd. 1967. Assigning meanings to programs. Mathematical Aspects of Computer Science 19 (1967), 19–33.

[35]

F. G. Foster. 1953. On the Stochastic Matrices Associated with Certain Queuing Processes. The Annals of Mathematical Statistics 24, 3 (1953), pp. 355–360.

[36]

Zoubin Ghahramani. 2015. Probabilistic machine learning and artificial intelligence. Nature 521, 7553 (2015), 452–459.

[37]

Laure Gonnord, David Monniaux, and Gabriel Radanne. 2015. Synthesis of Ranking Functions Using Extremal Counterexamples. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’15). ACM, New York, NY, USA, 608–618.

Digital Library

[38]

Friedrich Gretz, Joost-Pieter Katoen, and Annabelle McIver. 2014. Operational versus weakest pre-expectation semantics for the probabilistic guarded command language. Performance Evaluation 73 (2014), 110 – 132.

Digital Library

[39]

Sergiu Hart and Micha Sharir. 1985. Concurrent Probabilistic Programs, Or: How to Schedule if You Must. SIAM J. Comput. 14, 4 (1985), 991–1012.

[40]

L. P. Kaelbling, M. L. Littman, and A. W. Moore. 1996. Reinforcement learning: A survey. Journal of Artificial Intelligence Research 4 (1996), 237–285.

Digital Library

[41]

Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Federico Olmedo. 2016. Weakest Precondition Reasoning for Expected Run–Times of Probabilistic Programs. In Programming Languages and Systems: 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2–8, 2016, Proceedings, Peter Thiemann (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 364–389.

Digital Library

[42]

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, Vol. LNCS 6337, Springer. 390–406.

[43]

Dexter Kozen. 1981. Semantics of Probabilistic Programs. J. Comput. System Sci. 22, 3 (1981), 328–350.

[44]

Dexter Kozen. 1983. A Probabilistic PDL. In Proceedings of the Fifteenth Annual ACM Symposium on Theory of Computing (STOC ’83). ACM, New York, NY, USA, 291–297.

Digital Library

[45]

Daniel Kroening, Natasha Sharygina, Aliaksei Tsitovich, and Christoph M. Wintersteiger. 2010. Termination Analysis with Compositional Transition Invariants. In Computer Aided Verification: 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings, Tayssir Touili, Byron Cook, and Paul Jackson (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 89–103.

Digital Library

[46]

Marta Z. Kwiatkowska, Gethin Norman, and David Parker. 2011. PRISM 4.0: Verification of Probabilistic Real-Time Systems. In CAV (LNCS 6806). 585–591.

[47]

Chin Soon Lee, Neil D. Jones, and Amir M. Ben-Amram. 2001. The size-change principle for program termination. In POPL. 81–92.

Digital Library

[48]

Annabelle McIver and Carroll Morgan. 2004. Developing and Reasoning About Probabilistic Programs in pGCL. In PSSE. 123–155.

[49]

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

Digital Library

[50]

Annabelle McIver and Carroll Morgan. 2016. A new rule for almost-certain termination of probabilistic and demonic programs. CoRR abs/1612.01091 (2016). http://arxiv.org/abs/1612.01091

[51]

David Monniaux. 2001. An Abstract Analysis of the Probabilistic Termination of Programs. In Static Analysis, 8th International Symposium, SAS 2001, Paris, France, July 16-18, 2001, Proceedings (Lecture Notes in Computer Science), Patrick Cousot (Ed.), Vol. 2126. Springer, 111–126.

[52]

Rajeev Motwani and Prabhakar Raghavan. 1995. Randomized Algorithms. Cambridge University Press, New York, NY, USA.

[53]

M. Neuhäußer, M. Stoelinga, and J.-P. Katoen. 2009. Delayed Nondeterminism in Continuous-Time Markov Decision Processes. In Proceedings of FoSSaCS 2009, Vol. 5504. 364–379.

Digital Library

[54]

Martin R Neuhäußer and Joost-Pieter Katoen. 2007. Bisimulation and logical preservation for continuous-time Markov decision processes. In International Conference on Concurrency Theory (CONCUR 2007). Springer, 412–427.

[55]

Federico Olmedo, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. 2016. Reasoning About Recursive Probabilistic Programs. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS ’16). ACM, New York, NY, USA, 672–681.

Digital Library

[56]

Andreas Podelski and Andrey Rybalchenko. 2004a. A Complete Method for the Synthesis of Linear Ranking Functions. In Verification, Model Checking, and Abstract Interpretation, 5th International Conference, VMCAI 2004, Venice, January 11-13, 2004, Proceedings (Lecture Notes in Computer Science), Bernhard Steffen and Giorgio Levi (Eds.), Vol. 2937. Springer, 239–251.

[57]

Andreas Podelski and Andrey Rybalchenko. 2004b. Transition Invariants. In Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS ’04). IEEE Computer Society, Washington, DC, USA, 32–41.

[58]

Jeffrey S Rosenthal. 2006. A First Look at Rigorous Probability Theory (2nd ed.). World Scientific Publishing Company.

[59]

Micha Sharir, Amir Pnueli, and Sergiu Hart. 1984. Verification of Probabilistic Programs. SIAM J. Comput. 13, 2 (1984), 292–314.

Digital Library

[60]

Kirack Sohn and Allen Van Gelder. 1991. Termination Detection in Logic Programs using Argument Sizes. In Proceedings of the Tenth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, May 29-31, 1991, Denver, Colorado, USA, Daniel J. Rosenkrantz (Ed.). ACM Press, 216–226.

Digital Library

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
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
Gregersen SAguirre AHaselwarter PTassarotti JBirkedal L(2024)Almost-Sure Termination by Guarded RefinementProceedings of the ACM on Programming Languages10.1145/36746328:ICFP(203-233)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674632
Show More Cited By

Index Terms

Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs
1. Mathematics of computing
  1. Probability and statistics
    1. Stochastic processes
2. Theory of computation

Recommendations

Stochastic invariants for probabilistic termination
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

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 ...
Modular verification for almost-sure termination of probabilistic programs

In this work, we consider the almost-sure termination problem for probabilistic programs that asks whether a given probabilistic program terminates with probability 1. Scalable approaches for program analysis often rely on modularity as their theoretical ...
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 2, Issue POPL

January 2018

1961 pages

EISSN:2475-1421

DOI:10.1145/3177123

Issue’s Table of Contents

Copyright © 2017 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 27 December 2017

Published in PACMPL Volume 2, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Artifacts Evaluated & Functional

Author Tags

Qualifiers

Research-article

Funding Sources

Austrian Science Fund

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

44
Total Citations
View Citations
872
Total Downloads

Downloads (Last 12 months)176
Downloads (Last 6 weeks)24

Reflects downloads up to 09 Jan 2025

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
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
Gregersen SAguirre AHaselwarter PTassarotti JBirkedal L(2024)Almost-Sure Termination by Guarded RefinementProceedings of the ACM on Programming Languages10.1145/36746328:ICFP(203-233)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674632
Chatterjee KGoharshady AMeggendorfer TŽikelić Đ(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
https://dl.acm.org/doi/10.1145/3649824
Ye KWoodcock JFoster S(2024)Probabilistic unifying relations for modelling epistemic and aleatoric uncertaintyTheoretical Computer Science10.1016/j.tcs.2024.1148761021:COnline publication date: 21-Dec-2024
https://dl.acm.org/doi/10.1016/j.tcs.2024.114876
Hasuo IOyabu YEberhart CSuenaga KCho KKatsumata S(2024)Control-data separation and logical condition propagation for efficient inference on probabilistic programsJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2023.100922136(100922)Online publication date: Jan-2024
https://doi.org/10.1016/j.jlamp.2023.100922
Kassing JDollase SGiesl J(2024)A Complete Dependency Pair Framework for Almost-Sure Innermost Termination of Probabilistic Term RewritingFunctional and Logic Programming10.1007/978-981-97-2300-3_4(62-80)Online publication date: 15-May-2024
https://dl.acm.org/doi/10.1007/978-981-97-2300-3_4
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
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
Takisaka TZhang LWang CLiu J(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
https://dl.acm.org/doi/10.1007/978-3-031-65633-0_19
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

Media

Figures

Other

Tables

View Issue’s Table of Contents