Kaminski, BL;
Katoen, J-P;
Matheja, C;
Olmedo, F;
(2018)
Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms.
Journal of the ACM (JACM)
, 65
(5)
, Article 30. 10.1145/3208102.
Preview |
Text
main.pdf - Accepted Version Download (1MB) | Preview |
Abstract
This article presents a wp--style calculus for obtaining bounds on the expected runtime of randomized algorithms. Its application includes determining the (possibly infinite) expected termination time of a randomized algorithm 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 runtime 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 runtime of deterministic programs. We analyze the expected runtime of some example programs including the coupon collector’s problem, a one--dimensional random walk and a randomized binary search.
| Type: | Article |
|---|---|
| Title: | Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1145/3208102 |
| Publisher version: | https://doi.org/10.1145/3208102 |
| 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, Hardware & Architecture, Computer Science, Information Systems, Computer Science, Software Engineering, Computer Science, Theory & Methods, Computer Science, Probabilistic programs, expected runtime, positive almost-sure termination, weakest precondition, program verification, PROBABILISTIC TERMINATION, PROGRAMS, SEMANTICS, TIME |
| 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/10089685 |
Archive Staff Only
 |
View Item |
