TY - GEN
T1 - Safety verification of nonlinear hybrid systems based on invariant clusters
AU - Kong, Hui
AU - Bogomolov, Sergiy
AU - Schilling, Christian
AU - Jiang, Yu
AU - Henzinger, Thomas A.
N1 - Publisher Copyright:
© 2017 Copyright held by the owner/author(s). Publication rights licensed to ACM.
PY - 2017/4/13
Y1 - 2017/4/13
N2 - 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.
AB - 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.
KW - Hybrid system
KW - Invariant
KW - Nonlinear system
KW - SOS programming
KW - Safety verification
KW - Semialgebraic system
UR - http://www.scopus.com/inward/record.url?scp=85019027200&partnerID=8YFLogxK
U2 - 10.1145/3049797.3049814
DO - 10.1145/3049797.3049814
M3 - Conference contribution
T3 - HSCC 2017 - Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control (part of CPS Week)
SP - 163
EP - 172
BT - HSCC 2017 - Proceedings of the 20th International Conference on Hybrid Systems
PB - Association for Computing Machinery, Inc
T2 - 20th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2017
Y2 - 18 April 2017 through 20 April 2017
ER -