Sound Value Iteration for Simple Stochastic Games

1. Problem Statement

The paper addresses the challenge of computing precise reachability probabilities in Stochastic Games (SGs) and Markov Decision Processes (MDPs), particularly in systems containing End Components (ECs) (subsets of states where the system can remain indefinitely with probability 1).

• Context: Value Iteration (VI) is the standard algorithm for analyzing probabilistic systems due to its scalability. However, standard VI lacks precision guarantees; it converges to the exact value only in the limit, and intermediate iterations do not provide valid error bounds.
• Existing Solutions:
  • Bounded Value Iteration (BVI): Provides upper and lower bounds but converges slowly in the presence of probabilistic cycles (geometric convergence).
  • Sound Value Iteration (SVI): A previous method that provides tight bounds and converges significantly faster than BVI in systems with probabilistic cycles by using a geometric series extrapolation.
• The Gap: Previous SVI implementations were limited to MDPs/SGs without End Components. They failed to handle ECs because:
  1. Standard SVI relies on the assumption that the system eventually leaves the "unknown" states (which is false in ECs).
  2. Existing techniques for handling ECs in BVI (like "deflating" upper bounds) rely on maintaining explicit local upper bounds per state, whereas SVI uses a global bound derived implicitly from step-bounded probabilities.
  3. Directly applying deflation to SVI leads to non-termination or incorrect bounds due to cyclic dependencies and the inability to locally deflate a global bound.

2. Methodology

The authors propose a novel extension of SVI that handles both Stochastic Games and End Components. The methodology involves three main technical pillars:

A. Extension to Stochastic Games (No ECs)

Before tackling ECs, the authors generalize SVI from MDPs to SGs (involving Maximizer and Minimizer players).

• Strategy Construction: They define "k-step" strategies ($\sigma_k, \tau_k$) that optimize a specific objective: $P(\diamondsuit_{\le k} F) + P(\square_{\le k} S?) \cdot b_k$, where $b_k$ is the current bound.
• Decision Values: To ensure correctness when updating bounds, they introduce decision values. These are intersection points where the optimal action changes. The bounds are updated such that they do not cross these decision values, ensuring the chosen strategies remain optimal under the new bounds.

B. Handling End Components (ECs)

This is the core contribution. The authors identify that standard deflation fails in SVI and propose a new mechanism involving Best-Exit Sets (BES) and Delay Actions.

1. Best-Exit Set (BES):

   • Instead of collapsing ECs (which is impossible in SGs with different state values) or deflating the whole set, the algorithm recursively identifies Best Exits.
   • A recursive procedure (BestExitSet) decomposes the EC structure. It finds the "best" exit actions (those maximizing/minimizing the value) for sub-components.
   • This creates a hierarchical, attractor-like structure that breaks cyclic dependencies by identifying which states must eventually leave the EC to reach the target.

2. Delay Actions:

   • Problem: In ECs, updating values can lead to oscillation (e.g., the algorithm keeps shifting the "best exit" between two states without making progress).
   • Solution: The authors introduce a Delay Action ($d$). If updating a state's value would not improve the global upper bound (monotonicity check), the algorithm forces the player to play a "delay" action.
   • Effect: This action keeps the state unchanged but counts as a step. It prevents non-improving updates and ensures the sequence of upper bounds is monotonically non-increasing, guaranteeing convergence.

3. Modified Bellman Update:

   • The update rule is modified to prioritize:
     1. Delay Actions: If the upper bound would not improve.
     2. Best-Exit Actions: If the state is part of an EC and an exit is identified.
     3. Standard Actions: Otherwise.

C. Topological Improvements

The authors propose a topological variant where bounds are not computed globally over all unknown states ($S?$), but locally over the reachable states from a specific state (or Strongly Connected Component). This avoids "bad" states with high staying probabilities from dragging down the bounds for the entire system.

3. Key Contributions

1. Generalization of SVI: Successfully extended Sound Value Iteration to handle Stochastic Games and systems with End Components, overcoming a fundamental limitation of previous SVI work.
2. Novel EC Handling Mechanism: Introduced the Best-Exit Set and Delay Action concepts. This allows SVI to handle ECs without maintaining explicit local upper bounds, preserving the efficiency of the global bound approach.
3. Theoretical Proofs: Provided rigorous proofs for:
   • Correctness: The computed bounds are valid lower and upper bounds for the true value.
   • Convergence: The algorithm terminates and converges to the exact value, even in the presence of ECs, by proving the monotonicity of the upper bound sequence.
4. Topological Optimization: Proposed a method to compute bounds per SCC rather than globally, improving performance in large, complex state spaces.

4. Results

The authors implemented a prototype in PRISM-games and compared it against the standard BVI with deflating.

• Convergence Speed:
  • In systems with probabilistic cycles (geometric behavior), SVI converges significantly faster than BVI.
  • Example: In a specific benchmark, BVI required 685 iterations to reach precision $10^{-6}$, while SVI converged in just 2 iterations.
• Benchmark Performance:
  • On SG benchmarks, SVI required fewer iterations in 10 out of 40 cases, equal in 20, and more in 10. It excelled in benchmarks with probabilistic loops (e.g., haddad-monmege).
  • On MDP benchmarks, SVI generally outperformed BVI in non-trivial cases, though BVI performed slightly better in specific cases (e.g., wlan dl) where the decision value logic limited early bound improvements.
• Iteration Count: The primary metric of success was the reduction in the number of iterations required to achieve a target precision, demonstrating the efficiency of the geometric series extrapolation in SVI.

5. Significance

• Theoretical Foundation: The paper provides a deep theoretical understanding of how to handle cycles in SGs using value iteration. It highlights the inductive, attractor-like structure of MECs (Maximal End Components), offering a new perspective distinct from the "collapsing" or "deflating" approaches used in BVI.
• Complementarity: Rather than replacing BVI, this work complements it. BVI is efficient for "sure cycles" (deterministic loops), while this extended SVI is superior for "probabilistic cycles."
• Future Directions: The work opens the door for future enhancements to BVI by integrating SVI's efficient probabilistic cycle handling. It also suggests potential extensions to Concurrent Stochastic Games, a more complex class of games.
• Practical Impact: By providing a method that guarantees precision and converges faster in cyclic systems, this algorithm improves the reliability and efficiency of model checking tools for probabilistic systems.