A Simple and Efficient Statistical Model Checking Algorithm to Evaluate Markov Decision Processes

We propose a simple and efficient technique that allows the application of statistical model checking (SMC) to Markov Decision Processes (MDP). Our technique finds schedulers that transform the original MDP into a purely stochastic Markov Chain, on which standard SMC can be used. A statistical search is performed over the set of possible schedulers to find the best and worst with respect to the given property. If a scheduler is found that disproves the property, a counter-example is produced. If no counter-example is found, the algorithm concludes that the property is {\em probably} satisfied, with a confidence depending on the number of schedulers evaluated. Unlike previous approaches, the efficiency of our algorithm does not depend on structural properties of the MDP. Moreover, we have devised an efficient procedure to address general classes of schedulers by using Pseudo Random Number Generators and Hash Functions. In practice, our algorithm allows the representation of general schedulers in constant space, in contrast to existing algorithms that are exponential in the size of the system. In particular, this allows our SMC algorithm for MDPs to consider memory-dependant schedulers in addition to the memoryless schedulers that have been considered by others.