##
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)