Faster Convergence of Modified Policy Iteration for Quantitative Verification of Markov Decision Processes

Probabilistic model checking is a formal approach for verifying qualitative and quantitative properties of probabilistic and stochastic systems. Discrete-time Markov chains and Markov decision processes (MDPs) are used to modeling this class of systems. Reachability probabilities and expected costs are two classes of properties that are used to specify the requirements of probabilistic systems. Value iteration and policy iteration are well-known approaches for computing these classes of properties. In this paper, we consider MDPs with different levels of non-determinism. We show that modified policy iteration performs better than the other standard iterative methods when the degree of non-determinism increases. We propose several methods to improve the performance of the modified policy iteration method. Our approach is to define several criteria to avoid useless iterations and updates of the modified policy iteration method. As a result, the total numbers of iterations and updates are reduced, which results in an improvement in the performance of the method.