PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP

TL;DR

This paper introduces the first PAC algorithm for computing mean payoff in unknown MDPs and CTMDPs, requiring minimal prior knowledge and validated through experiments on benchmarks.

Contribution

It presents a novel PAC algorithm for mean payoff in unknown MDPs and extends it to CTMDPs, with minimal assumptions on the system.

Findings

Algorithm provides PAC bounds for mean payoff estimation.

Experimental results demonstrate practical effectiveness.

Requires only a lower bound on transition probabilities.

Abstract

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.