Sound Value Iteration for Simple Stochastic Games
For practitioners analyzing MDPs and SGs, this work removes previous limitations of SVI, enabling sound and efficient analysis of a broader class of models.
The paper extends sound value iteration (SVI) to stochastic games (SG) and Markov decision processes (MDP) with end components, providing guaranteed precision bounds and faster convergence on systems with probabilistic cycles. Experimental evaluation confirms advantages over existing methods.
Algorithmic analysis of Markov decision processes (MDP) and stochastic games (SG) in practice relies on value-iteration (VI) algorithms. Since the basic version of VI does not provide guarantees on the precision of the result, variants of VI have been proposed that offer such guarantees. In particular, sound value iteration (SVI) not only provides precise lower and upper bounds on the result, but also converges faster in the presence of probabilistic cycles. Unfortunately, it is neither applicable to SG, nor to MDP with end components. In this paper, we extend SVI and cover both cases. The technical challenge consists mainly in proper treatment of end components, which require different handling than in the literature. Moreover, we provide several optimizations of SVI. Finally, we also evaluate our prototype implementation experimentally to confirm its advantages on systems with probabilistic cycles.