What are the odds? Improving statistical model checking of Markov decision processes

Markov decision processes (MDPs) are a fundamental model of decision making which exhibit non-deterministic choice as well as probabilistic uncertainty. Traditionally, verification assumes exact knowledge of the probabilities that govern the behaviour of an MDP. However, this assumption often is unrealistic, e.g. when modelling cyber-physical systems or biological processes. There, we can employ statistical model checking (SMC) to obtain an estimate of the MDP’s value (e.g. the maximal probability of reaching a goal state) that is close to the true value with high confidence (probably approximately correct). Model-based SMC algorithms sample the MDP and build a model of it by estimating all transition probabilities, essentially for every transition answering the question: “What are the odds?” However, so far the statistical methods employed by state-of-the-art SMC verification algorithms are quite naive or even compromise the correctness guarantees. Our first contribution is to survey, categorize, and analyse statistical methods, identifying those few that are most efficient and that provide suitable guarantees for the verification setting. Secondly, we propose improvements that exploit structural knowledge of the MDP. Both contributions generalize to many types of problem statements as they are largely independent of the setting. Moreover, our experimental evaluation shows that they lead to significant gains, reducing the number of samples that an SMC algorithm has to collect by up to two orders of magnitude.