[WimmerBBHCHDT10]
Symblicit Calculation of Long-Run Averages for Concurrent
Probabilistic Systems
In Seventh International Conference on the Quantitative
Evaluation of Systems (QEST), pages 27-36, IEEE Computer Society, 2010.
Downloads: pdf, bibURL: http://dx.doi.org/10.1109/QEST.2010.12
Abstract. Model checkers for concurrent probabilistic systems have become
very popular within the last decade. The study of long-run average behavior
has however received only scant attention in this area, at least from the
implementation perspective. This paper studies the problem of how to
efficiently realize an algorithm for computing optimal long-run average reward
values for concurrent probabilistic systems. At its core is a variation of
Howard and Veinott's algorithm for Markov decision processes, where symbolic
and non-symbolic representations are intertwined in an effective manner: the
state space is represented using binary decision diagrams, while the linear
equation systems which have to be solved for the induced Markov chains to
improve the current scheduler are solved using an explicit state
representation. In order to keep the latter small, we apply a symbolic
bisimulation minimization algorithm to the induced Markov chain. The scheduler
improvement step itself is again performed on symbolic data structures.
Practical evidence shows that the implementation is effective, and sometimes
uses considerably less memory than a fully explicit implementation.