Sound Value Iteration Bounds

Context

Probabilistic model checkers often compute unbounded reachability probabilities by value iteration. Ordinary convergence tests can be unsound: two consecutive value vectors may be close while a large amount of probability mass is still trapped in slow transient structure. Sound Value Iteration adds a certificate for the remaining mass.

Formal Statement

For a Markov chain with absorbing goal set G, undecided set S?, and initial state s_I, define:

$$x_k(s)=P{r}_s({◊}_{\le k}G),y_k(s)=P{r}_s({\square }_{\le k}S?).$$

The decomposition is:

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

For states where y_k(s)<1, define lower and upper ratio bounds:

$${\ell }_k=\underset{s\in S?}{\min }\frac{x_k(s)}{1-y_k(s)},u_k=\underset{s\in S?}{\max }\frac{x_k(s)}{1-y_k(s)}.$$

Then:

$$x_k(s_I)+y_k(s_I){\ell }_k\le P{r}_{s_I}(◊G)\le x_k(s_I)+y_k(s_I)u_k.$$

The algorithm terminates when the interval width induced at s_I is below the requested tolerance.

For MDPs, the same structure is used with schedulers. The algorithm chooses actions maximizing x+y*u, tracks a decision value so that the scheduler remains valid for the proposed upper bound, and returns an epsilon-approximation for maximal reachability.

Derivation / Construction

• Run one value-iteration recurrence for step-bounded goal reachability.
• Run a second recurrence for the probability of remaining in the undecided region.
• Use the remaining undecided mass y_k to scale the worst-case lower/upper estimate of future reachability.
• In MDPs, update scheduler choices and reject upper bounds that would invalidate the actions chosen under the previous bound.
• The same decomposition lifts to expected reachability rewards by replacing reachability accumulation with reward accumulation before goal absorption.

Implications

• SVI converts approximate numerical model checking into an auditable bounded-error computation.
• It is especially important when the result is consumed by a safety filter, because an optimistic reachability underestimate can make a shield unsound.
• SVI is adjacent to interval iteration, but avoids precomputing starting vectors and often converges faster on benchmark models.
• The bound is about the explicit model; abstraction or model-learning error must be certified separately.

Links

• Quatmann2018 - Sound Value Iteration
• Sound Value Iteration
• Probabilistic Model Checking
• Probabilistic Shielding