Sound Policy Iteration

Abstract Reachability probabilities and expected rewards are two main classes of properties that are needed in the fields of reinforcement learning and formal verification. Value iteration and policy iteration are two iterative numerical method to compute the underlying properties. One of their drawbacks is that they only provide lower bounds for the computed values. To cover this challenge, some sound variations of value iteration have been proposed that also use upper bounds for their computed values and provide a guarantee for their soundness. In this paper, we focus on policy iteration and explain how this technique can be extended to provide sound values. For maximal expected reward, we use policy iteration to update lower bound values and apply action elimination for updating upper bounds. For minimal expected rewards, we apply policy iteration for upper bounds and action elimination for lower bounds. We employ some improved techniques to reduce the running time of our extension on policy iteration. We experimentally show that our proposed techniques outperform available sound value iteration techniques on the main part of standard case study models.