UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms

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. Green open access

[thumbnail of main.pdf]
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
Downloads since deposit
291Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item