Widest Path Games and Maximality Inheritance in Bounded Value Iteration for Stochastic Games

TL;DR

This paper introduces a new bounded value iteration algorithm for stochastic games based on widest path games, providing formal correctness proofs and demonstrating practical effectiveness in handling end components.

Contribution

It formalizes the core principles of widest path-based BVI, introduces 2WP-BVI algorithm, and proves its correctness using the maximality inheritance principle.

Findings

2WP-BVI performs well with numerous end components.

Theoretical foundations are rigorously established.

Experimental results show practical relevance.

Abstract

For model checking stochastic games (SGs), bounded value iteration (BVI) algorithms have gained attention as efficient approximate methods with rigorous precision guarantees. However, BVI may not terminate or converge when the target SG contains end components. Most existing approaches address this issue by explicitly detecting and processing end components--a process that is often computationally expensive. An exception is the widest path-based BVI approach previously studied by Phalakarn et al., which we refer to as 1WP-BVI. The method performs particularly well in the presence of numerous end components. Nonetheless, its theoretical foundations remain somewhat ad hoc. In this paper, we identify and formalize the core principles underlying the widest path-based BVI approach by (i) presenting 2WP-BVI, a clean BVI algorithm based on (2-player) widest path games, and (ii) proving its correctness using what we call the maximality inheritance principle--a proof principle previously employed in a well-known result in probabilistic model checking. Our experimental results demonstrate the practical relevance and potential of our proposed 2WP-BVI algorithm.