Improving Verification of Dense Markov Decision Processes

Value iteration is a powerful method for verification of quantitative properties of MDPs. In order to accelerating value iteration method many approaches have been proposed. Almost all of them try to avoid some unnecessary backups. But the performance of these methods depends on the graphical structure of MDP. Experimental results show that they don’t work much better than value iteration when the graph of MDP is dense. In this paper we present an algorithm which avoids unnecessary backups in dense MDPs while its overhead is small and the algorithm is easy to implement.

Keywords:

Quantitative verification , Markov decision processes , Probabilistic model checking