Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs

Abstract

This paper presents a wp-style calculus for obtaining bounds on the expected run-time of probabilistic programs. Its application includes determining the (possibly infinite) expected termination time of a probabilistic program 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 run-time 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 run-time of deterministic programs. We analyze the expected run-time of some example programs including a one-dimensional random walk and the coupon collector problem.

Cited by in corpus (8)

• Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Programs
• Formal verification of higher-order probabilistic programs
• Reasoning about Recursive Probabilistic Programs
• A new rule for almost-certain termination of probabilistic- and demonic programs
• New Approaches for Almost-Sure Termination of Probabilistic Programs
• Raising Expectations: Automating Expected Cost Analysis with Types
• Concentration-Bound Analysis for Probabilistic Programs and Probabilistic Recurrence Relations
• Fair Termination for Parameterized Probabilistic Concurrent Systems (Technical Report)