Computing Quantiles in Markov Chains with Multi-Dimensional Integer Costs

Christoph Haase

Probabilistic programs whose runs accumulate quantities such as energy or cost are naturally modelled by cost chains, which are Markov chains whose transitions are labelled with a vector of integer costs. Computing information on the probability distribution of the total cost accumulated along a run is a fundamental problem in this model. Central to the analysis and verification of certain probabilistic programs is the so-called cost problem, which is to compute quantiles of the total cost, such as the median cost or the probability of large costs. While it is an open problem whether such probabilities are always computable or even rational, in this talk I will present an algorithm that allows to approximate the probabilities with arbitrary precision. The algorithm is simple to state and implement, and exploits strong results from graph theory such as the so-called BEST theorem for efficiently computing the number of Eulerian circuits in a directed graph. Moreover, the algorithm allows for showing that the decision version of the cost problem lies in the counting hierarchy, a counting analogue to the polynomial-time hierarchy that contains the latter and is included in PSPACE. Finally, I will demonstrate the effectiveness of the algorithm by evaluating it on case studies of probabilistic programs that have appeared in the literature.

Joint work with S. Kiefer (Oxford) and M. Lohrey (Siegen)