Bisection Value Iteration

Probabilistic model checking is a powerful method for analyzing quantitative properties of probabilistic systems. Its core is to calculate reachability probabilities. One prevalent method of computing these probabilities is value iteration, which performs one-way fixed point iteration to obtain an approximation to the true value but sometimes returns unreliable results. Three recently proposed sound methods - interval iteration, sound value iteration and optimistic value iteration - extended from value iteration ensure the accuracy of the returned results, and each method has its own merits and demerits. In this paper, we propose a new sound method called bisection value iteration. Our method accelerates bounds convergence through bisection together with upper/lower bound verification and can be applied to calculating reachability and expected rewards for Markov decision processes. The experiments show that our method performs well on a wide range of instances.