Expected Runtime Analyis by Program Verification

Cambridge University Press eBooks, pp. 185–220

Abstract

This chapter is concerned with analysing the expected runtime of probabilistic programs by exploiting program verification techniques. We introduce a weakest pre-conditioning framework á la Dijkstra that enables to determine the expected runtime in a compositional manner. Like weakest pre-conditions, it is a reasoning framework at the syntax level of programs. Applications of the weakest pre-conditioning framework include determining the expected runtime of randomised algorithms, as well as determining whether a program is positive almost-surely terminating, i.e., whether the expected number of computation steps until termination is finite for every possible input. For Bayesian networks, a restricted class of probabilistic programs, we show that the expected runtime analysis can be fully automated. In this way, the simulation time under rejection sampling can be determined. This is particularly useful for ill-conditioned inference queries.

Authors 3

1. Benjamin Lucien Kaminski Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University

2. Joost-Pieter Katoen Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Germany

3. Christoph Matheja Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University