Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Sound Value Iteration for Simple Stochastic Games

Muqsit Azeem, Jan Kretinsky, Maximilian Weininger

TL;DR

This paper extends SVI and provides several optimizations of VI that are applicable to SG, nor to MDP with end components, and evaluates the prototype implementation experimentally to confirm its advantages on systems with probabilistic cycles.

Abstract

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.

Sound Value Iteration for Simple Stochastic Games

TL;DR

This paper extends SVI and provides several optimizations of VI that are applicable to SG, nor to MDP with end components, and evaluates the prototype implementation experimentally to confirm its advantages on systems with probabilistic cycles.

Abstract

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.

Paper Structure

This paper contains 33 sections, 19 theorems, 80 equations, 8 figures, 1 table, 7 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Value iteration and bounded value iteration
  4. Sound value iteration in Markov chains
  5. Sound value iteration for stochastic games without end components
  6. Computing the strategies
  7. Computing bounds
  8. Algorithm
  9. Extending sound value iteration to systems with end components
  10. Approximations do not converge in presence of ECs
  11. A sequence of difficulties: Why the natural solutions do not work
  12. Why do we need the delay action?
  13. Our solution
  14. Best exit set (BES)
  15. Delays and strategies
  16. ...and 18 more sections

Key Result

theorem 1

Let $\mathcal{M}$ be a Markov chain with probability measure $\mathcal{P}$ whose state space is partitioned into $\mathsf{F}$, $\mathsf{S}^?$ and $\mathsf{Z}$ as described above. Let $k\geq0$ such that $\mathcal{P} (\square^{\leq k} \mathsf{S}^?) < 1$ for all $s \in \mathsf{S}^?$. Then, for every st where $\mathsf{l}_k=\min_{s' \in \mathsf{S}^?} \frac{\mathcal{P}_{s'}(\lozenge^{\leq k} \mathsf{F})

Figures (8)

  • Figure 1: A Markov chain with an initial state $s$, a target state $\mathsf{f}$, and a sink/zero state $\mathsf{z}$
  • Figure 2: An SG with an EC $\{s_0,s_1\}$ and a sink $\mathsf{z}$
  • Figure 3: A game with trivial Maximizer EC
  • Figure 4: Game graph with two maximizer nodes and self-loops
  • Figure 5: An SG with $\mathsf{S}^?=\{p,q,r\}$
  • ...and 3 more figures

Theorems & Definitions (39)

  • definition 1: Stochastic Game (SG) DBLP:conf/dimacs/Condon90
  • definition 2: End component (EC) dA97a
  • definition 3: Best exit KKKW18
  • theorem 1
  • theorem 2
  • proof : Proof sketch
  • remark 1
  • theorem 3
  • lemma 1
  • theorem 4
  • ...and 29 more