Sciweavers

QEST
2010
IEEE

Symblicit Calculation of Long-Run Averages for Concurrent Probabilistic Systems

13 years 1 months ago
Symblicit Calculation of Long-Run Averages for Concurrent Probabilistic Systems
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 ag...
Ralf Wimmer, Bettina Braitling, Bernd Becker, Erns
Added 14 Feb 2011
Updated 14 Feb 2011
Type Journal
Year 2010
Where QEST
Authors Ralf Wimmer, Bettina Braitling, Bernd Becker, Ernst Moritz Hahn, Pepijn Crouzen, Holger Hermanns, Catuscia Dhama, Oliver E. Theel
Comments (0)