What Are the Odds? Improving the foundations of Statistical Model Checking

arXiv:2404.05424v1 Announce Type: cross
Abstract: 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 …

abstract algorithms arxiv cs.ai cs.lg cs.sy decision decision making eess.sy improving knowledge making markov processes statistical type uncertainty verification