Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Safe Reach Set Computation via Neural Barrier Certificates

Alessandro Abate, Sergiy Bogomolov, Alec Edwards, Kostiantyn Potomkin, Sadegh Soudjani, Paolo Zuliani

TL;DR

The paper tackles online safety verification for autonomous systems by learning barrier certificates with neural networks to over-approximate reach sets. It introduces a two-level framework with a MetaNN that generalizes barrier certificates across different initial and unsafe regions, trained offline via simulation data and validated online with SMT solvers to ensure soundness. Key contributions include leveraging level sets of barrier certificates as safe reach-set over-approximations, a data-generation pipeline using FOSSIL, and a MetaNN-driven online planning loop that outperforms direct FOSSIL usage in both success rate and speed (e.g., increasing online certificate generation from 78% to 99%). The approach enables sound online reachability for both linear and nonlinear systems, including an autonomous driving scenario, with practical implications for real-time safety-critical control. All mathematical statements and constraints are expressed with explicit barrier conditions and Lie derivatives, ensuring rigorous safety guarantees under the proposed framework.

Abstract

We present a novel technique for online safety verification of autonomous systems, which performs reachability analysis efficiently for both bounded and unbounded horizons by employing neural barrier certificates. Our approach uses barrier certificates given by parameterized neural networks that depend on a given initial set, unsafe sets, and time horizon. Such networks are trained efficiently offline using system simulations sampled from regions of the state space. We then employ a meta-neural network to generalize the barrier certificates to state space regions that are outside the training set. These certificates are generated and validated online as sound over-approximations of the reachable states, thus either ensuring system safety or activating appropriate alternative actions in unsafe scenarios. We demonstrate our technique on case studies from linear models to nonlinear control-dependent models for online autonomous driving scenarios.

Safe Reach Set Computation via Neural Barrier Certificates

TL;DR

The paper tackles online safety verification for autonomous systems by learning barrier certificates with neural networks to over-approximate reach sets. It introduces a two-level framework with a MetaNN that generalizes barrier certificates across different initial and unsafe regions, trained offline via simulation data and validated online with SMT solvers to ensure soundness. Key contributions include leveraging level sets of barrier certificates as safe reach-set over-approximations, a data-generation pipeline using FOSSIL, and a MetaNN-driven online planning loop that outperforms direct FOSSIL usage in both success rate and speed (e.g., increasing online certificate generation from 78% to 99%). The approach enables sound online reachability for both linear and nonlinear systems, including an autonomous driving scenario, with practical implications for real-time safety-critical control. All mathematical statements and constraints are expressed with explicit barrier conditions and Lie derivatives, ensuring rigorous safety guarantees under the proposed framework.

Abstract

We present a novel technique for online safety verification of autonomous systems, which performs reachability analysis efficiently for both bounded and unbounded horizons by employing neural barrier certificates. Our approach uses barrier certificates given by parameterized neural networks that depend on a given initial set, unsafe sets, and time horizon. Such networks are trained efficiently offline using system simulations sampled from regions of the state space. We then employ a meta-neural network to generalize the barrier certificates to state space regions that are outside the training set. These certificates are generated and validated online as sound over-approximations of the reachable states, thus either ensuring system safety or activating appropriate alternative actions in unsafe scenarios. We demonstrate our technique on case studies from linear models to nonlinear control-dependent models for online autonomous driving scenarios.
Paper Structure (10 sections, 3 theorems, 9 equations, 8 figures, 1 table)

This paper contains 10 sections, 3 theorems, 9 equations, 8 figures, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Barrier Certificates for Reach Sets
  4. Computation of Safe Reach Sets
  5. Simulation Engine
  6. Training of the MetaNN
  7. Simulation Results
  8. Linear system with real eigenvalues
  9. Linear system with complex eigenvalues.
  10. Discussion and Conclusions

Key Result

Theorem 2.1

BCPrajnaJ04prajna2007FrameworkWorstCaseStochastic Given the initial set $\mathcal{X}_0$ and unsafe set $\mathcal{X}_u$, the system eq:system is safe if there exists a barrier certificate $B(\cdot)$ satisfying the conditions eq:barrier.

Figures (8)

  • Figure 1: The proposed framework has two phases: (i) a training phase (top) where the training data is prepared and the MetaNN is trained; and (ii) a deployment phase (bottom) where sound reach sets are generated via neural barrier certificates. $\mathcal{X}_0=$ initial set; $\mathcal{X}_u=$ unsafe set; $\mathcal{X}_b=$ working region; $BC$= barrier certificate.
  • Figure 2: Structure of online safe planning scheme. The base controller (yellow) operates in normal conditions, while the safe controller (purple) is activated to avoid unsafe regions in case of potential hazard. The MetaNN is already trained. The Verifier checks the barrier certificate (BC) candidate and calls the safe controller in case the result is unsafe. Then the process of generating a BC candidate and running the simulation engine repeats and the new candidate is checked. If the system is unsafe or the MetaNN fails to generate a valid BC within the time bound the system stops.
  • Figure 3: Four-step construction of a safe reach set $R_b$. From the left-hand side: Step 1. Running simulations from the initial set $X_0$. Step 2. Computation of the octagonal over-approximation of the simulations. Step 3. Bloating of the octagonal over-approximation. Step 4. Computation of reachable set $R_b$.
  • Figure 4: Linear system with real eigenvalues.
  • Figure 5: Linear system with complex eigenvalues.
  • ...and 3 more figures

Theorems & Definitions (6)

  • Definition 1
  • Definition 2
  • Theorem 2.1
  • Corollary 3.1
  • Theorem 3.1
  • Remark 1