Sound Value Iteration

TL;DR

This paper introduces a new method for computing reachability probabilities in probabilistic model checking that provides tight bounds without initial vectors, converges faster, and is scalable based on extensive benchmarks.

Contribution

It presents a novel approach to reachability probability computation that avoids the need for initial vectors and improves convergence speed.

Findings

Method computes tight bounds cheaply

Converges faster than existing techniques

Demonstrates scalability on large benchmarks

Abstract

Computing reachability probabilities is at the heart of probabilistic model checking. All model checkers compute these probabilities in an iterative fashion using value iteration. This technique approximates a fixed point from below by determining reachability probabilities for an increasing number of steps. To avoid results that are significantly off, 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 computation is cheap - on the reachability probabilities. Lifting this technique to expected rewards is trivial for both Markov chains and MDPs. Experimental results on a large set of benchmarks show its scalability and efficiency.