PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP
Markov decision processes (MDP) and continuous-time MDP (CTMDP) are the
fundamental models for non-deterministic systems with probabilistic
uncertainty. Mean payoff (a.k.a. long-run average reward) is one of the most
classic objectives considered in their context. We provide the first algorithm
to compute mean payoff probably approximately correctly in unknown MDP;
further, we extend it to unknown CTMDP. We do not require any knowledge of the
state space, only a lower bound on the minimum transition probability, which
has been advocated in literature. In addition to providing probably
approximately correct (PAC) bounds for our algorithm, we also demonstrate its
practical nature by running experiments on standard benchmarks.