Automated Tail Bound Analysis for Probabilistic Recurrence Relations
Yican Sun, Hongfei Fu, Krishnendu Chatterjee, Amir Kafshdar Goharshady
摘要
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.
问问这篇 Paper
智能体会读完全文。
Lune 把这篇 Paper 索引到了每一个公式,引用它的顶会 Paper 也一样。你提问,回答直接引用原文。
引用它的顶会 Paper5
- Asparagus: Automated Synthesis of Parametric Gas Upper-Bounds for Smart ContractsZhuo Cai, Soroush Farokhnia, Amir Kafshdar Goharshady, S. HitarthOOPSLA 2023 · 被引用 16 次
- Quantitative Supermartingale CertificatesAlessandro Abate, Mirco Giacobbe, Diptarko RoyCAV 2025 · 被引用 7 次
- Denotational Foundations for Expected Cost AnalysisPedro H. Azevedo de AmorimOOPSLA 2025 · 被引用 4 次
- Practical Approximate Quantifier Elimination for Non-linear Real ArithmeticS. Akshay, Supratik Chakraborty, Amir Kafshdar Goharshady, R. Govind 等FM 2024 · 被引用 3 次
- Probabilistic Floating-Point Round-Off Analysis via Concentration InequalitiesYichen Tao, Hongfei Fu, Jiawei Chen, Jean-Baptiste JeanninOOPSLA 2026
它引用的顶会 Paper5
- Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic ProgramsKrishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer, Dorde ZikelicCAV 2022 · 被引用 30 次
- A pre-expectation calculus for probabilistic sensitivityAlejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski 等POPL 2021 · 被引用 24 次
- A Calculus for Amortized Expected RuntimesKevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja 等POPL 2023 · 被引用 22 次
- Quantitative analysis of assertion violations in probabilistic programsJinyi Wang, Yican Sun, Hongfei Fu, Krishnendu Chatterjee 等PLDI 2021 · 被引用 18 次
- Central moment analysis for cost accumulators in probabilistic programsDi Wang, Jan Hoffmann, Thomas W. RepsPLDI 2021 · 被引用 18 次
相关 Paper
- Dynaplex: analyzing program complexity using dynamically inferred recurrence relationsDidier Ishimwe, KimHao Nguyen, ThanhVu NguyenOOPSLA 2021 · 被引用 16 次
- Quantitative Bounds on Resource Usage of Probabilistic ProgramsKrishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer, Dorde ZikelicOOPSLA 2024 · 被引用 16 次
- Piecewise Analysis of Probabilistic Programs via 𝑘-InductionTengshun Yang, Shenghua Feng, Hongfei Fu, Naijun Zhan 等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 次
