Document Type: Original Research Paper

Author

Department of Computer science, Faculty of Mathematical Sciences, Vali-e-Asr University ofRafsanjan, Rafsanjan, Iran

Abstract

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.

Keywords

Main Subjects

[1] C. Baier and J.P. Katoen, Principles of Model Checking, MIT press, 2008.
[2] Y. Feng, Y. Nengkun, and M. Ying, “Model checking quantum Markov chains,” Journal of Computer and System Sciences, vol.79, no. 7, pp. 1181-1198, 2013.
[3] G. Norman, D. Parker, M. Kwiatkowska, S. Shukla, and R. Gupta,“Using probabilistic model checking for dynamic power management,” Formal Aspects of Computing, vol. 17, no. 2, pp.160-176, 2005.
[4] M. Kwiatkowska and C. Thachuk, “Probabilistic model checking for biology,” Software Systems Safety, vol. 36, pp. 165-189, 2014.
[5] T. Chen, F. Vojtch, M. Kwiatkowska, D. Parker, and A. Simaitis.“Automatic verification of competitive stochastic systems,” Formal Methods in System Design, vol. 43, no. 1, pp. 61-92,
2013.
[6] M. Kwiatkowska, G. Norman, and D. Parker, “Probabilistic verification of Hermans self-stabilisation algorithm,” Formal Aspects of Computing, vol. 24, no. 4, pp. 661-670, 2012.
[7] M. Kwiatkowska, G. Norman, and D. Parker, “Probabilistic model checking: advances and applications,” in Formal System Verification, pp. 73-121, Springer, Cham, 2018.
[8] N. Kamaleson, “Model reduction techniques for probabilistic verification of Markov chains,” Ph.D. Diss., University of Birmingham, 2018.
[9] M. Kwiatkowska, G. Norman, and D. Parker, “PRISM 4.0: verification of probabilistic real-time systems,” presented at the International conference on computer aided verification,
Berlin, Heidelberg, Germany, 2011.
[10] J. Sun, Y. Liu, J.S Dong, and J. Pang, “PAT: Towards flexible verification under fairness,” presented at the International Conference on Computer Aided Verification, Berlin,
Heidelberg, Germany, 2009.
[11] C. Dehnert, S. Junges, J.P. Katoen, and M. Volk, “A storm is coming: A modern probabilistic model checker,” presented at the International Conference on Computer Aided Verification,Berlin, Heidelberg, Germany, 2017.
[12] V. Forejt, M. Kwiatkowska, G. Norman, and D. Parker, “Automated verification techniques for probabilistic systems,” presented at the International School on Formal Methods for
the Design of Computer, Communication and Software Systems, Berlin, Heidelberg, Germany, 2011.
[13] A. Bianco and L. De Alfaro, “Model checking of probabilistic and nondeterministic systems,” presented at the International Conference on Foundations of Software Technology and
Theoretical Computer Science, Berlin, Heidelberg, Germany, 1995.
[14] H. Rashidi and M. Sadeghzadeh Hemayati, “Software quality models: A comprehensive review and analysis,” Journal of Electrical and Computer Engineering Innovations, vol. 6, no. 1,
pp. 59-76, 2018.
[15] A. Saberi Nejad and R. Tavoli “A method for estimating the cost of software using principle components analysis and data mining,” Journal of Electrical and Computer Engineering
Innovations, vol. 6, no. 1, pp. 33-42, 2018.
[16] M. L. Puterman and C. S. Moon, “Modified policy iteration algorithms for discounted Markov decision problems,” Management Science, vol. 24, no. 11, pp. 1127-1137, 1978.
[17] M. Kwiatkowska, D. Parker, and H. Qu, “Incremental quantitative verification for Markov decision processes,” in Proc. IEEE/IFIP 41st International Conference on Dependable
Systems & Networks (DSN), pp. 359-370, 2011.
[18] C. Baier, J. Klein, L. Leuschner, D. Parker, and S. Wunderlich, “Ensuring the reliability of your model checker: Interval iteration for markov decision processes,” in Proc. International
Conference on Computer Aided Verification, pp. 160-180, 2017.
[19] T. Brzdil, K. Chatterjee, M. Chmelk, V. Forejt, J. Ketnsk, M. Kwiatkowska, D. Parker, and M. Ujma, “Verification of Markov decision processes using learning algorithms,” in Proc.
International Symposium on Automated Technology for Verification and Analysis, pp. 98-114, 2014.
[20] M. Kwiatkowska, G. Norman, and D. Parker, “Symmetry reduction for probabilistic model checking,” in Proc. International Conference on Computer Aided Verification, pp.
234-248, 2006.
[21] M. Groesser and C. Baier, “Partial order reduction for Markov decision processes: A survey,” in Proc. International Symposium on Formal Methods for Components and Objects, pp.408-427, 2005.

[22] O. Shlakhter, “Acceleration of iterative methods for Markov decision processes,” Ph.D.Diss., 2010.
[23] D. Wingate and D. Kevin, “Prioritization methods for accelerating MDP solvers,” Journal of Machine Learning Research, vol. 6, no. 5 pp. 851-881, 2005.
[24] M. Mohagheghi, J. Karimpour, and A. Isazadeh. “Prioritizing methods to accelerate probabilistic model checking of discrete-time Markov models,” The Computer Journal, vol. 63, no. 1, pp. 105-122, 2020.
[25] J. Klein, C. Baier, P. Chrszon, and M. Daum, “Advances in probabilistic model checking with PRISM: Variable reordering, quintiles and weak deterministic Buchi automata,” International Journal on Software Tools for Technology Transfer, vol. 20, no. 2, pp. 179-194. 2018.
[26] L. Feng, “On learning assumptions for compositional verification of probabilistic systems,” Ph.D. Thesis, University of Oxford, October 2013.
[27] F. Ciesinski, C. Baier, M. Größer, and J. Klein, “Reduction techniques for model checking Markov decision processes,” in Proc. IEEE 2008 Fifth International Conference on Quantitative Evaluation of Systems, pp. 45-54, 2008.