Name
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. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1007/978-3-662-49498-1_15 | European Symposium on Programming |
Keywords | Field | DocType |
Probabilistic programs, Expected run-time, Positive almost-sure termination, Weakest precondition, Program verification | Predicate transformer semantics,Computer science,Random walk,Theoretical computer science,Coupon collector's problem,Probabilistic logic,Soundness,Conservative extension,Bounding overwatch | Journal |
Volume | ISSN | Citations |
abs/1601.01001 | 0302-9743 | 29 |
PageRank | References | Authors |
0.93 | 16 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Benjamin Lucien Kaminski | 1 | 126 | 10.46 |
| Joost-Pieter Katoen | 2 | 4444 | 289.65 |
| Christoph Matheja | 3 | 68 | 4.92 |
| Federico Olmedo | 4 | 130 | 6.18 |