Cone-Based Abstract Interpretation for Nonlinear Positive Invariant Synthesis

We present an abstract interpretation approach for synthesizing nonlinear (semi-algebraic) positive invariants for systems of polynomial ordinary differential equations (ODEs) and switched systems. The key behind our approach is to connect the system under study to a positive nonlinear system through a "change of variables". The positive invariance of the first orthant (<Formula format="inline"><TexMath><?TeX R₊?></TexMath><AltText>Math 1</AltText><File name="hscc24-10-inline1" type="svg"/></Formula>) for a positive system guarantees, in turn, that the functions involved in the change of variables define a positive invariant for the original system. The challenge lies in discovering such functions for a given system. To this end, we characterize positive invariants as fixed points under an operator that is defined using the Lie derivative. Next, we use abstract-interpretation approaches to systematically compute this fixed point. Whereas abstract interpretation has been applied to the static analysis of programs, and invariant synthesis for hybrid systems to a limited extent, we show how these approaches can compute fixed points over cones generated by polynomials using sum-of-squares optimization and its relaxations. Our approach is shown to be promising over a set of small but hard-to-analyze nonlinear models, wherein it is able to generate positive invariants to place useful bounds on their reachable sets.