PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games

Abstract

Statistical model checking (SMC) is a technique for analysis of probabilistic systems that may be (partially) unknown. We present an SMC algorithm for (unbounded) reachability yielding probably approximately correct (PAC) guarantees on the results. We consider both the setting (i) with no knowledge of the transition function (with the only quantity required a bound on the minimum transition probability) and (ii) with knowledge of the topology of the underlying graph. On the one hand, it is the first algorithm for stochastic games. On the other hand, it is the first practical algorithm even for Markov decision processes. Compared to previous approaches where PAC guarantees require running times longer than the age of universe even for systems with a handful of states, our algorithm often yields reasonably precise results within minutes, not requiring the knowledge of mixing time or the topology of the whole model.

References in corpus (5)

• UPPAAL-SMC: Statistical Model Checking for Priced Timed Automata
• Statistical Model Checking for Stochastic Hybrid Systems
• PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games
• Certified Reinforcement Learning with Logic Guidance
• Of Cores: A Partial-Exploration Framework for Markov Decision Processes

Cited by in corpus (14)

• PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games
• Robust Control for Dynamical Systems With Non-Gaussian Noise via Formal Abstractions
• Sampling-Based Robust Control of Autonomous Systems with Non-Gaussian Noise
• Widest Paths and Global Propagation in Bounded Value Iteration for Stochastic Games
• Sound Statistical Model Checking for Probabilities and Expected Rewards (extended version)
• Model-Free Reinforcement Learning for Stochastic Games with Linear Temporal Logic Objectives
• Comparison of Algorithms for Simple Stochastic Games (Full Version)
• Comparison of Algorithms for Simple Stochastic Games
• Learning Optimal Strategies for Temporal Tasks in Stochastic Games
• 1-2-3-Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization
• Reachability of Linear Uncertain Systems: Sampling Based Approaches
• Stochastic Games with Disjunctions of Multiple Objectives (Technical Report)
• Stochastic Games with Disjunctions of Multiple Objectives
• Statistically Model Checking PCTL Specifications on Markov Decision Processes via Reinforcement Learning