Accelerating Interval Iteration For Expected Rewards In Markov Decision Processes

Reachability probabilities and expected rewards are two important classes of properties that are computed in probabilistic model checking. Iterative numerical methods are used to compute these properties. Interval iteration and sound value iteration are proposed in recent years to guarantee the precision of computed values. These methods consider upper and lower bounds of values and update each bound in every iteration until satisfying the convergence criterion. In this paper, we focus on the computation of the expected rewards of models and propose two heuristics to improve the performance of the interval iteration method. The first heuristic updates the upper and lower bounds separately to avoid redundant updates. The second heuristic uses the computed values of the lower bound to approximate a starting point for the upper bound. We also propose a criterion for the correctness of the approximated upper bound. The experiments show that in most cases, interval iteration with our approaches outperforms the standard interval iteration and sound value iteration methods.