wiki

Sound Value Iteration

3 min read

Sound Value Iteration

Summary

This partial ingest is based on the extracted full PDF text. Quatmann and Katoen introduce Sound Value Iteration, a probabilistic model-checking algorithm that computes reachability probabilities and expected rewards with sound error bounds. Standard value iteration approaches a fixed point from one side and can stop prematurely with badly wrong values. Sound value iteration maintains both step-bounded reachability probabilities and the probability of still being in unknown states after the step bound; from these it derives cheap lower and upper bounds without needing a priori starting vectors. The method extends from Markov chains to MDPs and is implemented in Storm.

Key Claims

  • The usual stopping rule for value iteration can be unsound for unbounded reachability because small changes between iterations do not imply small error.
  • Sound upper and lower bounds can be obtained during value iteration by separating the already-reached probability from the remaining probability mass.
  • Unlike interval iteration, the method does not require precomputed lower and upper starting vectors.
  • The same idea lifts to expected rewards, Gauss-Seidel value iteration, topological value iteration, and MDPs.
  • On the reported benchmarks, SVI usually requires fewer iterations and lower runtime than interval iteration while remaining sound.

Methods / Formalism

  • For a Markov chain, let G be absorbing goal states and S? the states whose reachability probability is not already decided.
  • After k iterations, maintain:
    • x_k(s)=Pr_s(\Diamond_{\le k} G), the probability of reaching G within k steps;
    • y_k(s)=Pr_s(\Box_{\le k} S?), the probability of staying inside the undecided region for k steps.
  • The key decomposition is:
  • Ratios of the form x_k(s)/(1-y_k(s)) give lower and upper bounds on the missing reachability probability inside S?; the result bounds the initial value as x_k(s_I)+y_k(s_I) * ell_k <= Pr(\Diamond G) <= x_k(s_I)+y_k(s_I) * u_k.
  • For MDPs, the algorithm chooses schedulers that maximize x + y*u, and it tracks a decision value so that the newly computed upper bound remains valid for the scheduler choices.
  • Sound Value Iteration Bounds records the reusable MC/MDP bound construction.

Evidence / Experiments

  • The authors implemented SVI for MCs and MDPs in Storm using sparse explicit data structures.
  • The evaluation covers 130 model/property instances from the PRISM benchmark suite, PRISM website cases, Markov automata from IMCA, and multi-objective MDPs.
  • With precision epsilon=10^-6, SVI converges faster and needs fewer iterations than interval iteration for almost all tested MC and MDP instances.
  • The paper reports about a 20 percent average speed-up and especially strong gains on difficult cases requiring many iterations.
  • The topological variant of SVI is the fastest sound variant in the reported comparison and can approach the runtime of standard unsound value iteration.

Connections

  • Supplies a key numerical ingredient for Probabilistic Shielding, where the safety layer needs an upper bound on unsafe reachability probability rather than a one-sided lower approximation.
  • Complements Distributional Value Iteration: SVI makes scalar reachability/reward value iteration sound, while DVI preserves whole return distributions for risk-sensitive queries.
  • Strengthens Probabilistic Model Checking by making the approximation certificate part of the value-iteration loop.
  • Useful whenever a downstream safety claim depends on a numerical MDP probability bound, not only on an optimized policy.

Open Questions

  • How does SVI interact with abstraction error when the MDP itself is a quotient or learned model?
  • Can the same bound logic be adapted to neural approximate dynamic programming without losing soundness?
  • Which probabilistic shielding pipelines should use SVI versus interval iteration or optimistic value iteration?
  • How should SVI certificates be exposed to users so that downstream safety filters remain auditable?

Citation

Quatmann, Tim, and Joost-Pieter Katoen. 2018. “Sound Value Iteration.” In Computer Aided Verification (CAV 2018), LNCS 10981, 643-661.

Graph View

Backlinks