Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs
Preprint
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.Keywords
All Related Versions
This publication has 7 references indexed in Scilit:
- Runtime analysis of probabilistic programs with unbounded recursionJournal of Computer and System Sciences, 2015
- A probability perspectiveFormal Aspects of Computing, 2010
- A general framework for sound and complete Floyd-Hoare logicsACM Transactions on Computational Logic, 2009
- Universal Algebra for Computer Scientists1992
- Automating program analysisJournal of the ACM, 1988
- A hoare-like proof system for analysing the computation time of programsScience of Computer Programming, 1987
- An axiomatic basis for computer programmingCommunications of the ACM, 1969