Exact Safety Verification of Interval Hybrid Systems Based on Symbolic-Numeric Computation

TL;DR

This paper presents a hybrid symbolic-numeric method utilizing SOS relaxation and interval arithmetic to precisely verify safety properties of interval hybrid systems, including non-polynomial cases, demonstrated through benchmark experiments.

Contribution

It introduces an exact safety verification approach for interval hybrid systems using symbolic-numeric techniques, extending to non-polynomial systems.

Findings

Efficient verification of interval hybrid systems demonstrated on benchmarks.

Method produces exact inequality invariants for safety verification.

Applicable to non-polynomial hybrid systems.

Abstract

In this paper, we address the problem of safety verification of interval hybrid systems in which the coefficients are intervals instead of explicit numbers. A hybrid symbolic-numeric method, based on SOS relaxation and interval arithmetic certification, is proposed to generate exact inequality invariants for safety verification of interval hybrid systems. As an application, an approach is provided to verify safety properties of non-polynomial hybrid systems. Experiments on the benchmark hybrid systems are given to illustrate the efficiency of our method.