Learning Algorithms for Verification of Markov Decision Processes
Tomáš Brázdil, Krishnendu Chatterjee, Martin Chmelik, Vojtěch Forejt, Jan Křetínský, Marta Kwiatkowska, Tobias Meggendorfer, David Parker, Mateusz Ujma
TL;DR
The paper tackles the challenge of verifying unbounded probabilistic reachability in Markov decision processes with nondeterminism, including very large or unknown models. It introduces a unified learning-based framework that yields epsilon-optimal lower and upper bounds under two regimes: complete information via bound-aware, asynchronous techniques like BRTDP and interval iteration, and limited information via PAC-model-free learning (DQL) with sampling and delayed updates. A key methodological advance is the on-the-fly handling of end components through MEC collapsing, enabling correct convergence without requiring full graph exploration. The work unifies several strands of verification and learning, extending to stochastic games and providing theoretical guarantees (convergence, correctness, PAC bounds) while connecting to practical tooling and prior interval-based approaches. Overall, it offers a scalable, principled path to unbounded verification in large or black-box MDPs, bridging exact and statistical methods with rigorous end-component treatment.
Abstract
We present a general framework for applying learning algorithms and heuristical guidance to the verification of Markov decision processes (MDPs). The primary goal of our techniques is to improve performance by avoiding an exhaustive exploration of the state space, instead focussing on particularly relevant areas of the system, guided by heuristics. Our work builds on the previous results of Br{á}zdil et al., significantly extending it as well as refining several details and fixing errors. The presented framework focuses on probabilistic reachability, which is a core problem in verification, and is instantiated in two distinct scenarios. The first assumes that full knowledge of the MDP is available, in particular precise transition probabilities. It performs a heuristic-driven partial exploration of the model, yielding precise lower and upper bounds on the required probability. The second tackles the case where we may only sample the MDP without knowing the exact transition dynamics. Here, we obtain probabilistic guarantees, again in terms of both the lower and upper bounds, which provides efficient stopping criteria for the approximation. In particular, the latter is an extension of statistical model-checking (SMC) for unbounded properties in MDPs. In contrast to other related approaches, we do not restrict our attention to time-bounded (finite-horizon) or discounted properties, nor assume any particular structural properties of the MDP.