Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms

2018/08/29 by Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja +1 · 88 citations
Computer Science · #Algorithm #Artificial intelligence #Bounding overwatch #Complexity and Algorithms in Graphs #Computer science #Conservative extension #Formal Methods in Verification #Logic, programming, and type systems #Predicate transformer semantics #Programming language #Randomized algorithm #Simple (philosophy) #Soundness #Theoretical computer science

paper · open access · doi:10.1145/3208102

published in Journal of the ACM 65(5), 1-68 (Association for Computing Machinery)

openalex publication_date 2018/08/29 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/25

Abstract

This article presents a wp--style calculus for obtaining bounds on the expected runtime of randomized algorithms. Its application includes determining the (possibly infinite) expected termination time of a randomized algorithm and proving positive almost--sure termination—does a program terminate with probability one in finite expected time? We provide several proof rules for bounding the runtime of loops, and prove the soundness of the approach with respect to a simple operational model. We show that our approach is a conservative extension of Nielson’s approach for reasoning about the runtime of deterministic programs. We analyze the expected runtime of some example programs including the coupon collector’s problem, a one--dimensional random walk and a randomized binary search.

Cited by

• The annotated dependency pair framework for almost-sure termination of probabilistic term rewriting
• Relatively Complete Verification of Probabilistic Programs
• A Denotational Product Construction for Temporal Verification of Effectful Higher-Order Programs
• Traq: Estimating the Quantum Cost of Classical Programs
• To Zip Through the Cost Analysis of Probabilistic Programs
• Supermartingales, Ranking Functions and Probabilistic Lambda Calculus
• Dependency Pairs for Expected Innermost Runtime Complexity and Strong Almost-Sure Termination of Probabilistic Term Rewriting
• Runtime Analysis of Quantum Programs: A Formal Approach
• Tail Probabilities for Randomized Program Runtimes via Martingales for Higher Moments
• Quantitative Analysis of Assertion Violations in Probabilistic Programs
• Supermartingale Certificates for Quantitative Omega-regular Verification and Control
• Initial Algebra Correspondence under Reachability Conditions
• Positive Almost-Sure Termination of Polynomial Random Walks
• Reasoning about Recursive Quantum Programs
• A Cost-Aware Probability Monad for Liquid Haskell
• Supermartingales for Unique Fixed Points: A Unified Approach to Lower Bound Verification
• PrIC3: Property Directed Reachability for MDPs [europepmc]
• Inferring Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes [europepmc]
• Automated Termination Analysis of Polynomial Probabilistic Programs [europepmc]

Related

• Weakest Precondition Reasoning for Expected Run-Times of Probabilistic\n Programs
• Proving time bounds for randomized distributed algorithms
• Computing Expected Runtimes for Constant Probability Programs
• Reasoning about Recursive Probabilistic Programs
• Runtime Analysis of Probabilistic Programs with Unbounded Recursion