Kong, HuiBogomolov, SergiySchilling, ChristianYu, JiangHenzinger, Thomas A2021-09-14April 18-29781450345903http://hdl.handle.net/1885/247845In this paper, we propose an approach to automatically compute invariant clusters for nonlinear semialgebraic hybrid systems. An invariant cluster for an ordinary differential equation (ODE) is a multivariate polynomial invariant g(u, x)=0, parametric in u, which can yield an infinite number of concrete invariants by assigning different values to u so that every trajectory of the system can be overapproximated precisely by the intersection of a group of concrete invariants. For semialgebraic systems, which involve ODEs with multivariate polynomial right-hand sides, given a template multivariate polynomial g(u, x), an invariant cluster can be obtained by first computing the remainder of the Lie derivative of g(u,x) divided by g(u, x) and then solving the system of polynomial equations obtained from the coefficients of the remainder. Based on invariant clusters and sum-of-squares (SOS) programming, we present a new method for the safety verification of hybrid systems. Experiments on nonlinear benchmark systems from biology and control theory show that our approach is efficientThis research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award), and by the ARC project DP140104219 (Robust AI Planning for Hybrid Systems).application/pdfen-AU© 2017 Copyright held by the owner/author(s). Publication rights licensed to ACMhybrid systemnonlinear systemsemialgebraic systeminvariantsafety verificationSOS programming201710.1145/3049797.30498142020-11-23