  In this paper, we propose an approach to automatically compute invariant
clusters for 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 a union of concrete invariants. For semialgebraic
systems, which involve ODEs with multivariate polynomial vector flow, invariant
clusters can be obtained by first computing the remainder of the Lie derivative
of a template multivariate polynomial w.r.t. its Groebner basis 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 effective and efficient.
