@inproceedings{663,
  abstract     = {In 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 efficient. },
  author       = {Kong, Hui and Bogomolov, Sergiy and Schilling, Christian and Jiang, Yu and Henzinger, Thomas A},
  booktitle    = {Proceedings of the 20th International Conference on Hybrid Systems},
  isbn         = {978-145034590-3},
  location     = {Pittsburgh, PA, United States},
  pages        = {163 -- 172},
  publisher    = {ACM},
  title        = {{Safety verification of nonlinear hybrid systems based on invariant clusters}},
  doi          = {10.1145/3049797.3049814},
  year         = {2017},
}