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.
Cite
@article{arxiv.1601.01001,
title = {Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs},
author = {Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Federico Olmedo},
journal= {arXiv preprint arXiv:1601.01001},
year = {2022}
}