Policy Iteration in Finite Templates Domain

We prove in this paper that policy iteration can be generally defined in finite domain of templates using Lagrange duality without any assumption on the templates. Such policy iteration algorithm always converges to a fixed point under a very simple technical condition. This fixed point furnishes a safe over-approximation of the set of reachable values taken by the variables of a program. The paper also discusses the choice of good templates and links these good templates to invariant algebraic relations. When templates are well chosen, the policy iteration algorithm developed in this paper can be easily initialised for one single loop programs.