Exact Safety Verification of Hybrid Systems Using Sums-Of-Squares Representation

TL;DR

This paper introduces a hybrid symbolic-numeric approach using sum-of-squares relaxation to generate exact polynomial invariants for safety verification of hybrid systems, combining numerical optimization with rational recovery.

Contribution

It presents a novel method that computes exact inductive invariants for hybrid systems by integrating SOS relaxation with rational coefficient recovery, ensuring precise safety verification.

Findings

Successfully computes exact invariants for complex hybrid systems.

Demonstrates the effectiveness of the method on multiple examples.

Achieves precise safety verification through rational invariant recovery.

Abstract

In this paper we discuss how to generate inductive invariants for safety verification of hybrid systems. A hybrid symbolic-numeric method is presented to compute inequality inductive invariants of the given systems. A numerical invariant of the given system can be obtained by solving a parameterized polynomial optimization problem via sum-of-squares (SOS) relaxation. And a method based on Gauss-Newton refinement and rational vector recovery is deployed to obtain the invariants with rational coefficients, which exactly satisfy the conditions of invariants. Several examples are given to illustrate our algorithm.