Mohammadsadegh Mohagheghi - Departement of Computer Science, Vali-e-asr Rafsanjan University

Markov Decision Processes (MDPs) are used to model both non-deterministic and probabilistic systems. Probabilistic model checking is an approach for verifying quantitative properties of probabilistic systems that are modeled by MDPs. Value and Policy Iteration and modified version of them are well-known approaches for computing a wide range of probabilistic properties. This paper tries to improve the performance of modified policy iteration. Our approach is to use some information of the related model for approximating a good value for the number of iterations for each policy and improving this approximation in next modifications of policies.

Software Verification, Formal methods, Model checking, Probabilistic Systems