Accelerating Iterative Methods for Bounded Reachability Probabilities in Markov Decision Processes

Document Type : Software Engineering-Bagheri

Author

• Mohammadsadegh Mohagheghi

Department of Computer science, Vali-e-Asr University of Rafsanjan, Rafsanjan, Iran.

10.22067/cke.2020.39288

Abstract

Probabilistic model checking is a formal method for verification of the quantitative and qualitative properties of computer systems with stochastic behaviors. Markov Decision Processes (MDPs) are well-known formalisms for modeling this class of systems. Bounded reachability probabilities are an important class of properties that are computed in probabilistic model checking. Iterative numerical computations are used for this class of properties. A significant draw-back of the standard iterative methods is the redundant computations that do not affect the final results of the computations, but increase the running time of the computations. The study proposes two new approaches to avoid redundant computations for bounded reachability analysis. The general idea of these approaches is to identify and avoid useless numerical computations in iterative methods for computing bounded reachability probabilities.

Keywords

• Probabilistic model checking
• Iterative numerical methods
• Bounded Reachability probabilities
• Markov decision processes

---

References

References

[1] C. Baier, L. de Alfaro and V. Forejt. “Probabilistic Model Checking”, Dependable Software Systems Engineering, Vol. 45, pp. 1-23, 2016.

[2] C. Baier and J. Katoen. “Principles of model checking” MIT Press, USA. 2008.

[3] C. Baier, J. Klein, L. Leuschner, D. Parker and S. Wunderlich, “Ensuring the reliability of your model checker: Interval iteration for Markov Decision Processes”,  International Conference on Computer Aided Verification, Springer Cham, Vol. 27, pp. 160-180. 2017.

[4] T. Brazdil, K. Chatterjee, M. Chmelik, V. Forejt, J. Kretinsky, M. Kwiatkowska, D. Parker and M. Ujma. “Verification of Markov decision processes using learning algorithms”, International Symposium on Automated Technology for Verification and Analysis, Vol. 12, pp. 98-114. 2014

[5] F. Ciesinski, C. Baier, M. Gromer and J. Klein. “Reduction techniques for model checking Markov decision processes”, Fifth International Conference on Quantitative Evaluation of Systems, pp. 45-54. 2008.

[6] L. De Alfaro. “Formal verification of probabilistic systems.” PhD thesis. Stanford University, US, 1997.

[7] C. Dehnert, S. Junges, J. Katoen and M. Volk. “A storm is coming: A modern probabilistic model checker”, International Conference on Computer Aided Verification, pp. 592-600. Springer. 2017.

[8] V. Forejt, M. Kwiatkowska, G. Norman and D. Parker. “Automated Verification Techniques for Probabilistic Systems”,  InSFM, Vol. 11, pp. 53-113. 2011.

[9] L. Gui, J. Sun, S. Song, Y. Liu and J.S. Dong. “SCC-based improved reachability analysis for Markov decision processes”, In: International Conference on Formal Engineering Methods, pp. 171-186. Springer.

[10] E.M. Hahn, Y. Li, S. Schewe, A. Turrini and L. Zhang. “iscas M c: a web-based probabilistic model checker”,  International Symposium on Formal Methods, Springer. pp. 312-317. 2014.

[11] A. Hartmanns. “On the analysis of stochastic timed systems”, PhD thesis. Saarland University, Germany. 2015.

[12] A. Hartmanns and H. Hermanns. “The modest toolset: an integrated environment for quantitative modeling and verification”. International Conference on Tools and Algorithms for the Construction and Analysis of Systems,Springer. pp. 593-598. 2014.

[13] J. Katoen. “The probabilistic model checking landscape”. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, Vol. 5, pp. 31-45. 2013.

[14] M. Kattenbelt, M. Kwiatkowska, G. Norman and D. Parker. “Abstraction refinement for probabilistic software”, In: International Workshop on Verification, Model Checking, and Abstract Interpretation, Springer. pp. 182-197. 2009.

[15] J. Klein, C. Baier, P. Chrszon, M. Daum, C. Dubslaf, S. Kluppelholz, S. Marcker and D. Muller. “Advances in probabilistic model checking with PRISM: variable reordering, quantiles and weak deterministic Buchi automata”. International Journal on Software Tools for Technology Transfer, Vol. 20(2), pp. 179-194. 2018.

[16] M. Kwiatkowska, G. Norman and D. Parker. ”symmetry reduction for probabilistic model checking”,  International Conference on Computer Aided Verification, Springer. pp. 234-248. 2006.

[17] M. Kwiatkowska, G. Norman and D. Parker. “The PRISM benchmark suite”, 9th International Conference on Quantitative Evaluation of SysTems, IEEE CS press. pp. 203-204. 2010.

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

[19] M. L. Puterman. “Markov decision processes: Discrete stochastic dynamic programming”, In: Journal of the Operational Research Society, Vol. 46(6), pp. 792-792. 1994.

[20] T. Quatmann and J. Katoen. “Sound value iteration”, International Conference on Computer Aided Verification, Springer, Vol. 27, pp. 643-661. 2018.

[21] M. Ujma. “On verification and controller synthesis for probabilistic systems at runtime”, Ph.D. thesis, University of Oxford. 2015.