Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Converse Barrier Certificates for Finite-time Safety Verification of Continuous-time Perturbed Deterministic Systems

Yonghan Li, Chenyu Wu, Taoran Wu, Shijie Wang, Bai Xue

Abstract

In this paper, we investigate the problem of verifying the finite-time safety of continuous-time perturbed deterministic systems represented by ordinary differential equations in the presence of measurable disturbances. Given a finite-time horizon, if the system is safe, it, starting from a compact initial set, will remain within an open and bounded safe region throughout the specified time horizon, regardless of the disturbances. The main contribution of this work is a converse theorem: we prove that a continuously differentiable, time-dependent barrier certificate exists if and only if the system is safe over the finite-time horizon. The existence problem is explored by finding a continuously differentiable approximation of a unique Lipschitz viscosity solution to a Hamilton-Jacobi equation.

Converse Barrier Certificates for Finite-time Safety Verification of Continuous-time Perturbed Deterministic Systems

Abstract

In this paper, we investigate the problem of verifying the finite-time safety of continuous-time perturbed deterministic systems represented by ordinary differential equations in the presence of measurable disturbances. Given a finite-time horizon, if the system is safe, it, starting from a compact initial set, will remain within an open and bounded safe region throughout the specified time horizon, regardless of the disturbances. The main contribution of this work is a converse theorem: we prove that a continuously differentiable, time-dependent barrier certificate exists if and only if the system is safe over the finite-time horizon. The existence problem is explored by finding a continuously differentiable approximation of a unique Lipschitz viscosity solution to a Hamilton-Jacobi equation.
Paper Structure (6 sections, 10 theorems, 70 equations, 1 figure)

This paper contains 6 sections, 10 theorems, 70 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Related Work
  3. Preliminaries
  4. Converse Theorem for Safety Verification
  5. Examples
  6. Conclusion

Key Result

Proposition 1

If there exists a time-dependent barrier certificate $v$ satisfying Finite_safe, the system sys is safe over the time horizon $[0,T]$.

Figures (1)

  • Figure 1: Safety verification via barrier certificates for Example \ref{['ex1']}. The green curve denotes the initial set boundary $\partial\mathcal{X}_0$, the red curve shows the safe set boundary $\partial\mathcal{S}$, while the blue and pink curves represent the zero level sets of the barrier certificate at $t=0.5$ and $t=1.0$, respectively. All trajectories originating from $\mathcal{X}_0$ remain within the certified safe region bounded by the barrier level sets.

Theorems & Definitions (28)

  • Remark 1
  • Definition 1: Finite-time Safety Verification
  • Definition 2: Time-Dependent Barrier Certificates
  • Proposition 1
  • Lemma 1
  • proof
  • Lemma 2
  • proof
  • Lemma 3
  • proof
  • ...and 18 more