Sound Value Iteration

Definition

Sound value iteration is a value-iteration scheme for probabilistic model checking that returns an explicit error-bounded approximation rather than relying on successive-iterate convergence as a proxy for correctness.

Why It Matters

Unbounded reachability probabilities can converge slowly. Standard value iteration may appear stable while still being far from the true value, which is dangerous when the result is used as a safety certificate. Sound value iteration tracks the remaining undecided probability mass and turns the numerical loop into a proof-carrying approximation.

Formalism / Key Objects

• For goal states G and undecided states S?, SVI maintains two vectors:
  • x_k(s)=Pr_s(\Diamond_{\le k}G);
  • y_k(s)=Pr_s(\Box_{\le k}S?).
• The technical anchor is the decomposition:

$$Pr(◊G)=Pr({◊}_{\le k}G)+Pr(S?U_{>k}G).$$

• Bounds on the missing term are derived from ratios x_k(s)/(1-y_k(s)) over s in S?.
• In MDPs, SVI also tracks scheduler choices and decision values so that upper bounds remain valid under nondeterministic action choice.
• Sound Value Iteration Bounds stores the theorem-level MC/MDP bound details.

Connections

• A core method in Probabilistic Model Checking for reachability and expected-reward queries.
• Provides the kind of upper bound needed by Probabilistic Shielding when unsafe reachability must be bounded conservatively.
• Complements Distributional Value Iteration: SVI focuses on sound scalar bounds, while DVI preserves full return distributions.
• Relevant to Safe Reinforcement Learning when learned policies are wrapped by formal risk estimates.

Common Confusions

• SVI is not just value iteration with a smaller tolerance; it changes the stopping certificate.
• A sound numerical bound does not fix model abstraction error.
• SVI and interval iteration are both sound approaches, but SVI avoids precomputing initial bound vectors.

Key Sources

• Quatmann2018 - Sound Value Iteration
• Sound Value Iteration Bounds