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

2022/06/03 by Chaitanya Agarwal, Shibashis Guha, Agarwal, Chaitanya +5
Computer Science · #FOS: Computer and information sciences #FOS: Electrical engineering #Formal Methods in Verification #Machine Learning (cs.LG) #Petri Nets in System Modeling #Software Reliability and Analysis Research #Systems and Control (eess.SY) #electronic engineering #information engineering

paper · pdf · doi:10.48550/arxiv.2206.01465

openalex publication_date 2022/06/03 · openalex created_date 2022/06/13 · openalex updated_date 2026/07/28

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.

Related

• Learning and Planning in Average-Reward Markov Decision Processes
• Efficient Strategy Iteration for Mean Payoff in Markov Decision\n Processes
• Artifact for the paper "What are the Odds? Improving the Foundations of Statistical Model Checking"
• A Practitioner's Guide to MDP Model Checking Algorithms
• Multi-objective Optimization of Long-run Average and Total Rewards