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

Mohagheghi, M.S.

doi:10.22061/jecei.2020.5395.216

Document Type : Original Research Paper

Author

M.S. Mohagheghi

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

https://doi.org/10.22061/jecei.2020.5395.216

Abstract

Background and Objectives: Numerical iterative methods are widely used to compute reachability probabilities and expected rewards in probabilistic model checking of Markov decision processes. Several approaches have been proposed to improve the performance of these iterative methods. Reducing the total number of iterations is an important goal that is followed by several techniques in this paper.
Methods: 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 some novel 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. The first criterion considers the graphical structure of the model to define the number of iterations after each policy modification. The second criterion is a dynamic one to determine when a policy should be updated. The third proposed approach in this work is to use several priority heaps to select states for value updates.
Results: Our proposed methods are implemented in the PRISM model checker and applied on several standard case studies. The results of experiments show that the running times of our approaches are less than the running time of the standard and previous methods for most case studies. The main reason for these results is that the total numbers of iterations and updates are reduced by our approaches, which results in an improvement in the performance of the method. While the running times are reduced by our approaches, the precision of computations are kept in most cases.
Conclusion: The proposed techniques are able to reduce the number of iterations and accelerate the convergence to the optimal policies. The also prioritize the commutations to reduce the total number of updates.

Keywords

20.1001.1.23223952.2019.7.1.11.3

Main Subjects

Open Access

This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this license, visit: http://creativecommons.org/licenses/by/4.0/

Publisher’s Note

JECEI Publisher remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Publisher

Shahid Rajaee Teacher Training University

References

[1] C. Baier, J.P. Katoen, Principles of Model Checking, MIT press, 2008.

[2] Y. Feng, Y. Nengkun, M. Ying, “Model checking quantum Markov chains,” Journal of Computer and System Sciences, 79(7): 1181-1198, 2013.

[3] G. Norman, D. Parker, M. Kwiatkowska, S. Shukla, R. Gupta, “Using probabilistic model checking for dynamic power management,” Formal Aspects of Computing, 17(2): 160-176, 2005.

[4] M. Kwiatkowska, C. Thachuk, “Probabilistic model checking for biology,” Software Systems Safety, 36: 165-189, 2014.

[5] T. Chen, F. Vojtch, M. Kwiatkowska, D. Parker, A. Simaitis. “Automatic verification of competitive stochastic systems,” Formal Methods in System Design, 43(1): 61-92, 2013.

[6] M. Kwiatkowska, G. Norman, D. Parker, “Probabilistic verification of Hermans self-stabilisation algorithm,” Formal Aspects of Computing, 24(4): 661-670, 2012.

[7] M. Kwiatkowska, G. Norman, D. Parker, “Probabilistic model checking: advances and applications,” in Formal System Verification): 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, 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, 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, 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, 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, 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, M. Sadeghzadeh Hemayati, “Software quality models: A comprehensive review and analysis,” Journal of Electrical and Computer Engineering Innovations, 6(1): 59-76, 2018.

[15] A. Saberi Nejad, R. Tavoli “A method for estimating the cost of software using principle components analysis and data mining,” Journal of Electrical and Computer Engineering Innovations, 6(1): 33-42, 2018.

[16] M. L. Puterman, C. S. Moon, “Modified policy iteration algorithms for discounted Markov decision problems,” Management Science, 24(11): 1127-1137, 1978.

[17] M. Kwiatkowska, D. Parker, H. Qu, “Incremental quantitative verification for Markov decision processes,” in Proc. IEEE/IFIP 41st International Conference on Dependable Systems & Networks (DSN): 359-370, 2011.

[18] C. Baier, J. Klein, L. Leuschner, D. Parker, S. Wunderlich, “Ensuring the reliability of your model checker: Interval iteration for markov decision processes,” in Proc. International Conference on Computer Aided Verification: 160-180, 2017.

[19] T. Brzdil, K. Chatterjee, M. Chmelk, V. Forejt, J. Ketnsk, M. Kwiatkowska, D. Parker, M. Ujma, “Verification of Markov decision processes using learning algorithms,” in Proc. International Symposium on Automated Technology for Verification and Analysis): 98-114, 2014.

[20] M. Kwiatkowska, G. Norman, D. Parker, “Symmetry reduction for probabilistic model checking,” in Proc. International Conference on Computer Aided Verification: 234-248, 2006.

[21] M. Groesser, C. Baier, “Partial order reduction for Markov decision processes: A survey,” in Proc. International Symposium on Formal Methods for Components and Objects: 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, 6(5): 851-881, 2005.

[24] M. Mohagheghi, J. Karimpour, A. Isazadeh. “Prioritizing methods to accelerate probabilistic model checking of discrete-time Markov models,” The Computer Journal, 63(1): 105-122, 2020.

[25] J. Klein, C. Baier, P. Chrszon, 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, 20(2): 179-194. 2018.

[26] L. Feng, “On learning assumptions for compositional verification of probabilistic systems,” Ph.D. Thesis, University of Oxford, 2013.

[27] F. Ciesinski, C. Baier, M. Größer, J. Klein, “Reduction techniques for model checking Markov decision processes,” in Proc. IEEE 2008 Fifth International Conference on Quantitative Evaluation of Systems: 45-54, 2008.

LETTERS TO EDITOR

Journal of Electrical and Computer Engineering Innovations (JECEI) welcomes letters to the editor for the post-publication discussions and corrections which allows debate post publication on its site, through the Letters to Editor. Letters pertaining to manuscript published in JECEI should be sent to the editorial office of JECEI within three months of either online publication or before printed publication, except for critiques of original research. Following points are to be considering before sending the letters (comments) to the editor.

[1] Letters that include statements of statistics, facts, research, or theories should include appropriate references, although more than three are discouraged.

[2] Letters that are personal attacks on an author rather than thoughtful criticism of the author’s ideas will not be considered for publication.

[3] Letters can be no more than 300 words in length.

[4] Letter writers should include a statement at the beginning of the letter stating that it is being submitted either for publication or not.

[5] Anonymous letters will not be considered.

[6] Letter writers must include their city and state of residence or work.

[7] Letters will be edited for clarity and length.

Name *

Email Address *

Affiliation *

Comments *

Security Code *

Journal of Electrical and Computer Engineering Innovations (JECEI)

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

References

References

Send comment about this article

Volume 7, Issue 1
January 2019
Pages 113-122

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

References

References

Send comment about this article

Volume 7, Issue 1January 2019Pages 113-122

Volume 7, Issue 1
January 2019
Pages 113-122