Sound Value Iteration

Abstract

. Computing reachability probabilities is at the heart of prob- abilistic model checking. All model checkers compute these probabilities in an iterative fashion using value iteration. This technique approximates a xed point from below by determining reachability probabilities for an increasing number of steps. To avoid results that are signi cantly o , variants have recently been proposed that converge from both below and above. These procedures require starting values for both sides. We present an alternative that does not require the a priori computation of starting vectors and that converges faster on many benchmarks. The crux of our technique is to give tight and safe bounds whose computa- tion is cheap on the reachability probabilities. Lifting this technique to expected rewards is trivial for both Markov chains and MDPs. Exper- imental results on a large set of benchmarks show its scalability and e ciency.