Cone-based abstract interpretation for nonlinear positive invariant synthesis
(2024) 27th ACM International Conference on Hybrid Systems: Computation and Control — Location: Hong Kong, China (13.May.2024)
Files
36415133650127.pdf
Open Access - Adobe PDF
- 3.49 MB
Details
- Authors
- Abstract
- 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 $\mathbb{R}_+$ 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.
- Affiliations
Citations
Berger, G., Ghanbarpour, M., & Berger, G. (2024). Cone-based abstract interpretation for nonlinear positive invariant synthesis. Published. 27th ACM International Conference on Hybrid Systems: Computation and Control, Hong Kong, China. https://doi.org/10.1145/3641513.3650127