Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms

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 wi...

Full description

Saved in:
Bibliographic Details
Published in:Journal of the ACM 2018-09, Vol.65 (5), p.1-68, Article 30
Main Authors: Kaminski, Benjamin Lucien, Katoen, Joost-Pieter, Matheja, Christoph, Olmedo, Federico
Format: Article
Language:English
Subjects:
Algorithms
Cognition & reasoning
Formal software verification
Hoare logic
Invariants
Logic
Logic and verification
Mathematical problems
Models of computation
Operational semantics
Pre- and post-conditions
Probabilistic computation
Probability
Program reasoning
Program semantics
Program verification
Random walk
Randomization
Randomized algorithms
Reasoning
Run time (computers)
Semantics and reasoning
Software and its engineering
Software creation and management
Software verification and validation
Theory of computation
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0004-5411
1557-735X
DOI:10.1145/3208102