Efficient analysis of probabilistic systems that accumulate quantities

ABSTRACT. Probabilistic systems that accumulate quantities such as energy and/or cost are naturally modelled by Markov chains whose transitions are labelled with vectors of numbers. Computing information on the probability distribution of the total accumulated cost is a fundamental problem in this model. The naive way of solving this problem is to encode the accumulated quantities in the state space of the model, incurring an exponential blowup. One can improve on this approach. I will explain how results on Presburger arithmetic, language theory and graph theory lead to more efficient algorithms and verification tools. Joint work with Christoph Haase and Markus Lohrey.

Authors

• Stefan Kiefer

Keywords

No keywords are indexed for this paper.