Safety Verification of Nonlinear Autonomous System via Occupation Measures

TL;DR

This paper presents a novel method for safety verification of nonlinear autonomous systems by quantifying the time spent in unsafe regions through occupation measures and semidefinite programming, validated by simulations.

Contribution

It introduces a flexible safety verification approach using occupation measures and the Lasserre hierarchy for polynomial systems, providing converging bounds.

Findings

Monotonically converging bounds on unsafe region occupation times

Effective numerical validation through simulations

Framework applicable to polynomial nonlinear systems

Abstract

In this paper, we introduce a flexible notion of safety verification for nonlinear autonomous systems by measuring how much time the system spends in given unsafe regions. We consider this problem in the particular case of nonlinear systems with a polynomial dynamics and unsafe regions described by a collection of polynomial inequalities. In this context, we can quantify the amount of time spent in the unsafe regions as the solution to an infinite-dimensional linear program (LP). This LP measures the volume of the unsafe region with respect to the occupation measure of the system trajectories. Using Lasserre hierarchy, we approximate the solution to the infinite-dimensional LP using a sequence of finite-dimensional semidefinite programs (SDPs). The solutions to the SDPs in this hierarchy provide monotonically converging upper bounds on the optimal solution to the infinite-dimensional LP. Finally, we validate the performance of our framework using numerical simulations.