Improving modified policy iteration for probabilistic model checking

• Autorzy: Mohagheghi Mohammadsadegh , Karimpour Jaber , Isazadeh Ayaz

Identyfikatory

DOI

10.7494/csci.2022.23.1.4139

• Języki publikacji: EN

Abstrakty

EN

Along with their modified versions, value iteration and policy iteration are well-known algorithms for the probabilistic model checking of Markov decision processes. One challenge with 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 times of these techniques depend on the graphical structure of the utilized model. In some cases, their performance can be worse than the performance of standard methods. In this paper, we propose two new heuristics for accelerating 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 for identifying useless updates in each iteration. This method reduces the running time of the computations by avoiding the 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 times of previous standard and improved methods. Our experimental results show that our techniques yields a significant speed-up.

Słowa kluczowe

EN

probabilistic model checking; Markov decision processes; modified policy iteration; probabilistic reachability

• Wydawca: Wydawnictwa AGH
• Czasopismo: Computer Science
• Rocznik: 2022
• Tom: T. 23 (1)
• Strony: 63--80
• Opis fizyczny: Bibliogr. 21 poz., rys., tab.

Twórcy

autor

Mohagheghi Mohammadsadegh

• University of Tabriz, Department of Computer Science, Tabriz, Iran

• https://orcid.org/0000-0001-8059-3691+

autor

Karimpour Jaber

• University of Tabriz, Department of Computer Science, Tabriz, Iran

autor

Isazadeh Ayaz

• University of Tabriz, Department of Computer Science, Tabriz, Iran

Bibliografia

• [1] Ábrahám E., Jansen N., Wimmer R., Katoen J.P., Becker B.: DTMC model hecking by SCC reduction. In: 2010 Seventh International Conference on the uantitative Evaluation of Systems, pp. 37–46, IEEE, 2010.
• [2] Ashok P., Křetínsk`y J., Weininger M.: PAC statistical model checking for Markovdecision processes and stochastic games. In: International Conference on Computer Aided Verification, pp. 497–519, Springer, 2019.
• [3] Baier C., Hermanns H., Katoen J.P.: The 10,000 facets of MDP model checking. n: Computing and Software Science, pp. 420–451, Springer, 2019.
• [4] Baier C., Katoen J.P.: Principles of model checking, MIT Press, 2008.
• [5] Baier C., Klein J., Leuschner L., Parker D., Wunderlich S.: Ensuring the eliability of your model checker: Interval iteration for Markov decision processes. n: International Conference on Computer Aided Verification, pp. 160–180, pringer, 2017.
• [6] Brázdil T., Chatterjee K., Chmelik M., Forejt V., Křetínsk`y J., Kwiatkowska M., arker D., Ujma M.: Verification of Markov decision processes using learning algorithms. In: International Symposium on Automated Technology for Verification and Analysis, pp. 98–114, Springer, 2014.
• [7] Dehnert C., Junges S., Katoen J.P., Volk M.: A storm is coming: A modern probabilistic model checker. In: International Conference on Computer Aided Verification, pp. 592–600, Springer, 2017.
• [8] Feng L., Kwiatkowska M., Parker D.: Compositional verification of probabilistic systems using learning. In: 2010 Seventh International Conference on the Quantitative Evaluation of Systems, pp. 133–142, IEEE, 2010.
• [9] Forejt V., Kwiatkowska M., 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, pp. 53–113, Springer, 2011.
• [10] Gros T.P., Hermanns H., Hoffmann J., Klauck M., Steinmetz M.: Deep statistical model checking. In: International Conference on Formal Techniques for Distributed Objects, Components, and Systems, pp. 96–114, Springer, 2020.
• [11] Hartmanns A.: On the Analysis of Stochastic Timed Systems, Ph.D. thesis, Saarland University, 2015.
• [12] Katoen J.P.: The probabilistic model checking landscape. In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, pp. 31–45, 2016.
• [13] Klein J., Baier C., Chrszon P., Daum M., Dubslaff C., Klüppelholz S., Märcker S., Müller D.: Advances in probabilistic model checking with PRISM: variable reordering, quantiles and weak deterministic Büchi automata, International Journal on Software Tools for Technology Transfer, vol. 20(2), pp. 179–194, 2018.
• [14] Kwiatkowska M., Norman G., Parker D.: Symmetry reduction for probabilistic model checking. In: International Conference on Computer Aided Verification, pp. 234–248, Springer, 2006.
• [15] Kwiatkowska M., Norman G., Parker D.: PRISM 4.0: Verification of probabilistic real-time systems. In: International Conference on Computer Aided Verification, pp. 585–591, Springer, 2011.
• [16] Kwiatkowska M., Parker D., Qu H.: Incremental quantitative verification for Markov decision processes. In: 2011 IEEE/IFIP 41st International Conference on Dependable Systems & Networks (DSN), pp. 359–370, IEEE, 2011.
• [17] Mohagheghi M., Karimpour J., Isazadeh A.: Prioritizing methods to accelerate probabilistic model checking of discrete-time Markov models, The Computer Journal, vol. 63(1), pp. 105–122, 2020.
• [18] Parker D.A.: Implementation of symbolic model checking for probabilistic systems, Ph.D. thesis, University of Birmingham, 2003.
• [19] Puterman M.L.: Markov decision processes: discrete stochastic dynamic programming, John Wiley & Sons, 2014.
• [20] Rataj A., Woźna-Szcześniak B.: Extrapolation of an Optimal Policy using Statistical Probabilistic Model Checking, Fundamenta Informaticae, vol. 157(4), pp. 443–461, 2018.
• [21] Ujma M.: On verification and controller synthesis for probabilistic systems at runtime, Ph.D. thesis, Citeseer, 2015.

Uwagi

PL

Opracowanie rekordu ze środków MEiN, umowa nr SONP/SP/546092/2022 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2022-2023).