Prioritizing Methods to Accelerate Probabilistic Model Checking of Discrete-Time Markov Models

摘要

Probabilistic model checking is an automated technique for the verification of systems that exhibit stochastic behavior. Iterative numerical methods are usually used to solve quantitative verification problems of probabilistic models. In this paper, we consider Markov Decision Processes and propose three techniques to improve the performance of the iterative methods. While several methods have been proposed to improve the performance of the standard iterative methods, their performance depends on the structure of the models, and they are more useful for acyclic models. In contrast, we propose several heuristic methods to improve the performance of the standard iteration methods that are more useful for cyclic models. The first heuristic method prioritizes states according to their impact on the other states. The second prioritizes transitions according to their probability. In these two approaches, low priority states and transitions can be avoided in some iterations while the method reuses related values from the previous iteration. The third method reorders the information of the model to improve the memory access and reduce the impact of cache latency. Experimental results demonstrate that our methods outperform other iterative approaches for most case studies.