Coupling Policy Iteration with Piecewise Quadratic Lyapunov Functions to Overapproximate the Reachable Values Set of Piecewise Affine Discrete-Time Dynamical Systems.
Assalé Adjé · arXiv (Cornell University) · 2015
We have recently constructed a piecewise quadratic Lyapunov function to prove the boundedness of the values taken by the variables of a program with switches and affine updates. We have also extracted bounds on the reachable values during the computation of the piecewise quadratic Lyapunov function. In this paper, we refine the latter bounds using policy iteration. We also prove that the latter policy iteration converges to the smallest fixed point of the abstract semantics functional considering the templates basis composed of the square of the variables and the piecewise quadratic Lyapunov functional. We illustrate our techniques on various examples.