Value Iteration with Guessing for Markov Chains and Markov Decision Processes
Krishnendu Chatterjee, Mahdi JafariRaviz, Raimundo Saona, Jakub Svoboda
TL;DR
This work tackles the exponential barrier in Value Iteration for Markov Chains and Markov Decision Processes by introducing a guessing-based preprocessing that identifies a small set of states to fix with guessed values. For MCs, the authors achieve subexponential Bellman updates after an almost-linear preprocessing, using a level-based Interval VI framework and symbolic, graph-theoretic techniques. They also present an improved convergence analysis for VI in MDPs and a practical Guessing VI (GVI) algorithm implemented in STORM, with extensive benchmarking on the Quantitative Verification Benchmark Set showing notable speedups over existing VI-based approaches. The results demonstrate the practical viability of guessing and level-based strategies to significantly accelerate VI in both MCs and MDPs, while outlining open questions about polynomial-time preprocessing for MDPs and extensions to broader models such as stochastic games.
Abstract
Two standard models for probabilistic systems are Markov chains (MCs) and Markov decision processes (MDPs). Classic objectives for such probabilistic models for control and planning problems are reachability and stochastic shortest path. The widely studied algorithmic approach for these problems is the Value Iteration (VI) algorithm which iteratively applies local updates called Bellman updates. There are many practical approaches for VI in the literature but they all require exponentially many Bellman updates for MCs in the worst case. A preprocessing step is an algorithm that is discrete, graph-theoretical, and requires linear space. An important open question is whether, after a polynomial-time preprocessing, VI can be achieved with sub-exponentially many Bellman updates. In this work, we present a new approach for VI based on guessing values. Our theoretical contributions are twofold. First, for MCs, we present an almost-linear-time preprocessing algorithm after which, along with guessing values, VI requires only subexponentially many Bellman updates. Second, we present an improved analysis of the speed of convergence of VI for MDPs. Finally, we present a practical algorithm for MDPs based on our new approach. Experimental results show that our approach provides a considerable improvement over existing VI-based approaches on several benchmark examples from the literature.