Darboux-type barrier certificates for safety verification of nonlinear hybrid systems

Benefit from less computational difficulty, barrier certificate based method has attracted much attention in safety verification of hybrid systems. Barrier certificates are inherent existences of a hybrid system and may have different types. A set of well-defined verification conditions is a prerequisite for successfully identifying barrier certificates of a specific type. Therefore, how to define verification conditions that can identify barrier certificates invisible to existing conditions becomes an essential problem in barrier certificate based verification. This paper proposes a set of verification conditions that helps to construct a new type of barrier certificate, namely, the Darboux-type barrier certificate made of Darboux polynomial. The proposed verification conditions provide powerful aids in non-linear hybrid system verification as the Darboux-type barrier certificates can verify systems that may not be settled by existing verification conditions. Furthermore, we give a novel computational approach, combining the sampling-based relaxation method with least-squares and quadratic programming (LS-QP) alternating projection, to find Darboux-type barrier certificates. We demonstrate on the benchmark examples from the literature that our verification conditions can enhance the capability of barrier certificate based approaches through successfully verifying those systems that are difficult to be handled by existing verification conditions, and our algorithm is efficient.