Reduction Techniques for Model Checking Markov Decision Processes

The quantitative analysis of a randomized system, modeled by a Markov decision process, against an LTL formula can be performed by a combination of graph algorithms, automata-theoretic concepts and numerical methods to compute maximal or minimal reachability probabilities. In this paper, we present various reduction techniques that serve to improve the performance of the quantitative analysis, and report on their implementation on the top of the probabilistic model checker LiQuor. Although our techniques are purely heuristic and cannot improve the worst-case time complexity of standard algorithms for the quantitative analysis, a series of examples illustrates that the proposed methods can yield a major speed-up.