Output details

A game-based abstraction-refinement framework for Markov decision processes

<11>Presents a novel approach, based on stochastic games, for automatically constructing and analysing abstractions of Markov decision processes, a widely-used probabilistic model. Compared to existing approaches, abstractions yield more precise analysis results and, crucially, a quantitative measure of their precision. Experimental results show the technique to be highly effective. Follow-up research papers have shown its applicability to probabilistic hybrid automata, probabilistic software verification and probabilistic real-time systems, the latter leading to a major new release of the widely used PRISM tool. The approach has been taken up and extended by several other research groups (e.g. Saarland, Munich).