Automated Tail Bound Analysis for Probabilistic Recurrence Relations
Yican Sun, Hongfei Fu, Krishnendu Chatterjee, Amir Kafshdar Goharshady
Abstract
Abstract Probabilistic recurrence relations (PRRs) are a standard formalism for describing the runtime of a randomized algorithm. Given a PRR and a time limit κ , we consider the tail probability Pr [ T ≥ κ ] , i.e., the probability that the randomized runtime T of the PRR exceeds κ . Our focus is the formal analysis of tail bounds that aims at finding a tight asymptotic upper bound u ≥ Pr [ T ≥ κ ] . To address this problem, the classical and most well-known approach is the cookbook method by Karp (JACM 1994), while other approaches are mostly limited to deriving tail bounds of specific PRRs via involved custom analysis. In this work, we propose a novel approach for deriving the common exponentially-decreasing tail bounds for PRRs whose preprocessing time and random passed sizes observe discrete or (piecewise) uniform distribution and whose recursive call is either a single procedure call or a divide-and-conquer. We first establish a theoretical approach via Markov’s inequality, and then instantiate the theoretical approach with a template-based algorithmic approach via a refined treatment of exponentiation. Experimental evaluation shows that our algorithmic approach is capable of deriving tail bounds that are (i) asymptotically tighter than Karp’s method, (ii) match the best-known manually-derived asymptotic tail bound for QuickSelect, and (iii) is only slightly worse (with a log log n factor) than the manually-proven optimal asymptotic tail bound for QuickSort. Moreover, our algorithmic approach handles all examples (including realistic PRRs such as QuickSort, QuickSelect, DiameterComputation, etc.) in less than 0.1 s, showing that our approach is efficient in practice.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext 13dfdcb8-bb46-4440-bd75-f9446b62e494Cited by top-tier papers5
- Asparagus: Automated Synthesis of Parametric Gas Upper-Bounds for Smart ContractsZhuo Cai, Soroush Farokhnia, Amir Kafshdar Goharshady, S. HitarthOOPSLA 2023 · 16 citations
- Quantitative Supermartingale CertificatesAlessandro Abate, Mirco Giacobbe, Diptarko RoyCAV 2025 · 7 citations
- Denotational Foundations for Expected Cost AnalysisPedro H. Azevedo de AmorimOOPSLA 2025 · 4 citations
- Practical Approximate Quantifier Elimination for Non-linear Real ArithmeticS. Akshay, Supratik Chakraborty, Amir Kafshdar Goharshady, R. Govind et al.FM 2024 · 3 citations
- Probabilistic Floating-Point Round-Off Analysis via Concentration InequalitiesYichen Tao, Hongfei Fu, Jiawei Chen, Jean-Baptiste JeanninOOPSLA 2026
Builds on5
- Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic ProgramsKrishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer, Dorde ZikelicCAV 2022 · 30 citations
- A pre-expectation calculus for probabilistic sensitivityAlejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski et al.POPL 2021 · 24 citations
- A Calculus for Amortized Expected RuntimesKevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja et al.POPL 2023 · 22 citations
- Quantitative analysis of assertion violations in probabilistic programsJinyi Wang, Yican Sun, Hongfei Fu, Krishnendu Chatterjee et al.PLDI 2021 · 18 citations
- Central moment analysis for cost accumulators in probabilistic programsDi Wang, Jan Hoffmann, Thomas W. RepsPLDI 2021 · 18 citations
Related papers
- Dynaplex: analyzing program complexity using dynamically inferred recurrence relationsDidier Ishimwe, KimHao Nguyen, ThanhVu NguyenOOPSLA 2021 · 16 citations
- Quantitative Bounds on Resource Usage of Probabilistic ProgramsKrishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer, Dorde ZikelicOOPSLA 2024 · 16 citations
- Piecewise Analysis of Probabilistic Programs via 𝑘-InductionTengshun Yang, Shenghua Feng, Hongfei Fu, Naijun Zhan et al.POPL 2026
- Supermartingales for Unique Fixed Points: A Unified Approach to Lower Bound VerificationSatoshi Kura, Hiroshi Unno, Takeshi TsukadaPLDI 2026
- Adaptive Recursive Query OptimizationAnna Herlihy, Guillaume Martres, Anastasia Ailamaki, Martin OderskyICDE 2024 · 5 citations
