Automated Run-Time Analysis of Probabilistic ProgramsCopyright: Joost-Pieter Katoen
Randomization has been an important tool for the construction of algorithms since the early days of computing. It is typically used to convert a deterministic algorithm with bad worst case behaviour into an efﬁcient randomized algorithm that yields a correct output, possibly with a low error probability. The Rabin-Miller primality test, Freivalds’ matrix multiplication, and the random pivot selection in Hoare’s quicksort algorithm are prime examples. Randomized algorithms are conveniently described by probabilistic programs. The run-time of a randomized algorithm is a random variable as the run-time is affected by the outcome of the coin tosses. An important efﬁciency measure for probabilistic programs is the expected run-time. Reasoning about the expected run-time of randomized algorithms is surprisingly subtle and full of nuances. In classical sequential deterministic algorithms, a single diverging program run yields the program to have an inﬁnite run-time. This is not true for randomized algorithms. They may admit arbitrarily long and even inﬁnite runs while still having a ﬁnite expected run-time. The expected run-time of randomized algorithms is typically analysed using standard mathematical means. Recently there is some initial work towards applying formal veriﬁcation techniques to analyse the run-time of probabilistic programs. Alternative techniques are either based on using super-martingales, or a weakest pre-conditioning style reasoning. None of these techniques is fully automated. The goal of this dissertation project is to develop a fully automated technique for the inference of expected run-time bounds for probabilistic programs. This challenging objective will be approached by exploiting recently developed powerful techniques to infer upper and lower bounds for the run-time complexity of ordinary for example non-probabilistic programs. The plan is to extend these techniques for the automated complexity analysis of programs towards probabilistic programs, and combine them with the recent weakest precondition calculus of in order to generate suitable upper and lower invariants that are needed to infer expected run-times of probabilistic programs. Besides the theoretical developments, a prototypical implementation in the tool AProVE is planned. Extensive experiments will be carried out to analyse the expected run-time of well-known randomized algorithms such as Sherwood variants of binary search, quicksort and the challenging coupon collector problem. Given the connections between positive almost-sure terminations and expected run-times, there is an obvious link between the similar topics listed at the botton of this page.