Widest Paths and Global Propagation in Bounded Value Iteration for Stochastic Games

Abstract

Solving stochastic games with the reachability objective is a fundamental problem, especially in quantitative verification and synthesis. For this purpose, bounded value iteration (BVI) attracts attention as an efficient iterative method. However, BVI's performance is often impeded by costly end component (EC) computation that is needed to ensure convergence. Our contribution is a novel BVI algorithm that conducts, in addition to local propagation by the Bellman update that is typical of BVI, global propagation of upper bounds that is not hindered by ECs. To conduct global propagation in a computationally tractable manner, we construct a weighted graph and solve the widest path problem in it. Our experiments show the algorithm's performance advantage over the previous BVI algorithms that rely on EC computation.

v2: an URL to the implementation is added

References in corpus (5)

• PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games
• Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm
• A reduction from parity games to simple stochastic games
• Widest Paths and Global Propagation in Bounded Value Iteration for Stochastic Games
• Near-Linear Time Algorithms for Streett Objectives in Graphs and MDPs

Cited by in corpus (3)

• Widest Paths and Global Propagation in Bounded Value Iteration for Stochastic Games
• Value Iteration with Guessing for Markov Chains and Markov Decision Processes
• Widest Path Games and Maximality Inheritance in Bounded Value Iteration for Stochastic Games