Kaminski, BL;
Katoen, J-P;
Matheja, C;
Olmedo, F;
(2016)
Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs.
In: Thiemann, P, (ed.)
Proceedings of the 25th European Symposium on Programming (ESOP).
(pp. pp. 364-389).
Springer: Cham, Switzerland.
Preview |
Text
main.pdf - Accepted Version Download (547kB) | Preview |
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.
| Type: | Proceedings paper |
|---|---|
| Title: | Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs |
| Event: | 25th European Symposium on Programming (ESOP) Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS) |
| Location: | Eindhoven, NETHERLANDS |
| Dates: | 03 April 2016 - 07 April 2016 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1007/978-3-662-49498-1_15 |
| Publisher version: | https://doi.org/10.1007/978-3-662-49498-1_15 |
| Language: | English |
| Additional information: | This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions. |
| Keywords: | Science & Technology, Technology, Computer Science, Software Engineering, Computer Science, Theory & Methods, Computer Science, Probabilistic programs, Expected run-time, Positive almost-sure termination, Weakest precondition, Program verification |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10089692 |
Archive Staff Only
 |
View Item |
