Improving modified policy iteration for probabilistic model checking
Keywords:Probabilistic model checking, Markov decision processes, Modified policy iteration, Probabilistic reachability
Value iteration, policy iteration and their modified versions are well-known algorithms for probabilistic model checking of Markov Decision Processes. One the challenge of these methods is that they are time-consuming in most cases. Several techniques have been proposed to improve the performance of iterative methods for probabilistic model checking. However, the running time of these techniques depends on the graphical structure of the model and in some cases their performance is worse than the performance of the standard methods. In this paper, we propose two new heuristics to accelerate the modified policy iteration method. We first define a criterion for the usefulness of the computations of each iteration of this method. The first contribution of our work is to develop and use a criterion to reduce the number of iterations in modified policy iteration. As the second contribution, we propose a new approach to identify useless updates in each iteration. This method reduces the running time of computations by avoiding useless updates of states. The proposed heuristics have been implemented in the PRISM model checker and applied on several standard case studies. We compare the running time of our heuristics with the running time of previous standard and improved methods. Experimental results show that our techniques yields a significant speed-up.
Baier C., Hermanns H., Katoen JP. (2019) The 10,000 Facets of MDP Model Checking. In: Steffen B., Woeginger G. (eds) Computing and Software Science. Lecture Notes in Computer Science, vol 10000. Springer, Cham. https://doi.org/10.1007/978-3-319-91908-9 21.
Baier, C. and Katoen, J.-P. Principles of model checking, Cambridge, MA, USA: MIT Press, 2008
Katoen J.P. The probabilistic model checking landscape. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science; 5 July 2016. pp. 31-45.
Forejt V, Kwiatkowska MZ, Norman G, Parker D. Automated verification techniques for probabilistic Systems. In: International School on Formal Methods for the Design of Computer, Communication and Software Systems; 13 June 2011; Berlin, Heidelberg, Germany: Springer. pp. 53-113.
Puterman M. L. Markov decision processes: discrete stochastic dynamic programming. John Wiley & Sons. 28 August 2014.
Kwiatkowska M, Norman G, Parker D. PRISM 4.0: Verification of probabilistic real-time systems. In: Proceedings of 23-th International Conference on Computer Aided Verification. 14 July 2011; Snowbird, UT, USA,: LNCS, Springer. pp. 585-591.
Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, and Matthias Volk. A storm is coming: A modern probabilistic model checker. In: Proceedings of 29-th International Conference on Computer Aided Verification. 24-28 July 2017; Heidelberg, Berlin, Germany: LNCS, Springer. pp. 592-600.
Brzdil T, Chatterjee K, Chmelk M, Forejt V, Ketnsk J, Kwiatkowska M, Parker D, Ujma M. Verification of Markov decision processes using learning algorithms. In: Proceedings of 12th International Symposium on Automated Technology for Verification and Analysis; 3 November 2014; Sydney, Australia. pp. 98-114.
Rataj, Artur, and Bozena Wozna-Szczesniak. "Extrapolation of an Optimal Policy using Statistical Probabilistic Model Checking." Fundamenta Informaticae 157, no. 4 (2018): 443-461.
Kwiatkowska M, Parker D, Qu H. Incremental quantitative verification for Markov decision processes. In: proceedings of 41st IEEE/IFIP International Conference on Dependable Systems & Networks; IEEE, 27 June 2011; pp. 359-370.
Baier C, Klein J, Leuschner L, Parker D, Wunderlich S. Ensuring the reliability of your model checker: interval iteration for Markov decision processes. In: Proceedings of 29-th International Conference on Computer Aided Verification. 24-28 July 2017; Heidelberg, Germany: Springer. pp. 160-180.
Mohagheghi M, Karimpour J, Isazadeh A. Prioritizing methods to accelerate probabilistic model checking of discrete-time Markov models. The Computer Journal 63 (1), 2020. pp. 105-122
Parker D. Implementation of symbolic model checking for probabilistic systems. PhD thesis. University of Birmingham, 2003.
Klein J, Baier C, Chrszon P, Daum M, Dubslaff C, Klppelholz S, Mrcker S, Mller D. Advances in probabilistic model checking with PRISM: variable reordering, quintiles and weak deterministic Bchi automata. In: Int J Softw Tools Technol Transf 2017; 19: 1-16.
Feng L, KwiatkowskaM, Parker D. Compositional verification of probabilistic systems using learning. In: Proceedings of the 2010 Seventh International Conference on the Quantitative Evaluation of Systems; 15 September 2010; Williamsburg, VA, USA: IEEE. pp. 133-142.
Hartmanns, A. On the Analysis of Stochastic Timed Systems, Ph.D. Thesis, Universitt des Saarlandes, February 2015
Ashok P, Ketnsk J, Weininger M. PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games. In International Conference on Computer Aided Verification 2019 Jul 15 (pp. 497-519). Springer, Cham.
Kwiatkowska M, Norman G, Parker D. Symmetry reduction for probabilistic model checking. In: Proceedings of 18-th International Conference on Computer Aided Verification. 17-20 August 2006; Seattle, WA, USA: LNCS, Springer. pp. 160-180.
Ujma, Mateusz. On Verification and Controller Synthesis for Probabilistic Systems at Runtime. Ph.D. Thsis, University of Oxford, 2015.
Abrahm E, Jansen N, Wimmer R, Katoen JP, Becker B. DTMC model checking by SCC reduction. In: Quantitative Evaluation of Systems (QEST), Seventh International Conference; 15-18 September 2018; Williamsburg, VA, USA: IEEE pp. 37-46
Gros T.P., Hermanns H., Hoffmann J., Klauck M., Steinmetz M. (2020) Deep Statistical Model Checking. In: Gotsman A., Sokolova A. (eds) Formal Techniques for Distributed Objects, Components, and Systems. FORTE 2020. Lecture Notes in Computer Science, vol 12136. Springer, Cham. https://doi.org/10.1007/978-3-030-50086-3
How to Cite
Copyright (c) 2021 Computer Science
This work is licensed under a Creative Commons Attribution 4.0 International License.