Policy iteration in finite templates domain

ABSTRACT. We prove in this paper that policy iteration can be generally defined in finite templates domain 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, policy iteration developed in this paper can be easily initialised for one single loop programs.