Accelerating Iterative Methods for Bounded Reachability Probabilities in Markov Decision Processes

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.