A Sums-of-Squares Extension of Policy Iterations

TL;DR

This paper introduces a Sums-of-Squares extension to policy iteration methods, enabling more precise static analysis of polynomial systems with improved accuracy and broader applicability in control systems.

Contribution

It extends policy iteration to include SOS-based optimization, allowing analysis of polynomial programs beyond quadratic invariants with enhanced precision.

Findings

Implemented in Matlab and tested on control system programs.

Improves the range of analyzable systems.

Enhances analysis precision for polynomial systems.

Abstract

In order to address the imprecision often introduced by widening operators in static analysis, policy iteration based on min-computations amounts to considering the characterization of reachable value set of a program as an iterative computation of policies, starting from a post-fixpoint. Computing each policy and the associated invariant relies on a sequence of numerical optimizations. While the early research efforts relied on linear programming (LP) to address linear properties of linear programs, the current state of the art is still limited to the analysis of linear programs with at most quadratic invariants, relying on semidefinite programming (SDP) solvers to compute policies, and LP solvers to refine invariants. We propose here to extend the class of programs considered through the use of Sums-of-Squares (SOS) based optimization. Our approach enables the precise analysis of switched systems with polynomial updates and guards. The analysis presented has been implemented in Matlab and applied on existing programs coming from the system control literature, improving both the range of analyzable systems and the precision of previously handled ones.