Invariant Clusters for Hybrid Systems

TL;DR

This paper introduces a novel method for automatically computing invariant clusters in semialgebraic hybrid systems, enabling precise overapproximation of system trajectories and enhancing safety verification.

Contribution

It presents a new approach combining invariant clusters and SOS programming for safety verification of hybrid systems, with efficient computation techniques.

Findings

Effective on nonlinear biological and control systems benchmarks.

Enables precise overapproximation of system trajectories.

Demonstrates efficiency and effectiveness of the proposed method.

Abstract

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.