PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP
This work addresses the challenge of analyzing non-deterministic systems with probabilistic uncertainty for researchers and practitioners in formal verification and control theory, representing a novel advancement rather than an incremental improvement.
The authors tackled the problem of computing mean payoff in unknown Markov decision processes (MDP) and continuous-time MDP (CTMDP) without prior knowledge of the state space, achieving the first algorithm for this task with probably approximately correct (PAC) bounds and demonstrating its practicality through experiments on standard benchmarks.
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.