What Are the Odds? Improving the foundations of Statistical Model
  Checking
Tobias Meggendorfer Maximilian Weininger Patrick Wienhöft
Markov decision processes (MDPs) are a fundamental model for decision making
under uncertainty. They exhibit non-deterministic choice as well as
probabilistic uncertainty. Traditionally, verification algorithms assume exact
knowledge of the probabilities that govern the behaviour of an MDP. As this
assumption is often unrealistic in practice, statistical model checking (SMC)
was developed in the past two decades. It allows to analyse MDPs with unknown
transition probabilities and provide probably approximately correct (PAC)
guarantees on the result. 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 the state of the art SMC algorithms are quite
naive. Our contribution are several fundamental improvements to those methods:
On the one hand, we survey statistics literature for better concentration
inequalities; on the other hand, we propose specialised approaches that exploit
our knowledge of the MDP. Our improvements are generally applicable to many
kinds of problem statements because they are largely independent of the
setting. Moreover, our experimental evaluation shows that they lead to
significant gains, reducing the number of samples that the SMC algorithm has to
collect by up to two orders of magnitude.