Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Neural Network-assisted Interval Reachability for Systems with Control Barrier Function-Based Safe Controllers

Damola Ajeyemi, Saber Jafarpour, Emiliano Dall'Anese

TL;DR

The paper tackles runtime verification of safety-critical systems governed by control barrier functions (CBFs), where optimization-based safety filters can induce undesirable behaviors. It introduces a neural network–assisted interval reachability framework that replaces online optimization with a pre-trained neural network $\mathcal{N}(x)$ approximating the optimal input $v(x)$, and then embeds the NN-controlled system using inclusion functions to obtain interval bounds via mixed-monotone theory; a trajectory of the embedding system yields a hyper-rectangular over-approximation of the reachable set, which is further enlarged by a Minkowski-sum bound to account for approximation error. A key closeness result provides an explicit bound on the trajectory deviation between the true system and the NN-approximated system, enabling rigorous over-approximation of $\mathcal{R}_{fs}(t,\mathcal{X}_0)$. The method is demonstrated numerically on integrator and double-integrator scenarios with obstacles, showing efficient computation times and accurate containment of true trajectories, thus enabling real-time safety and performance verification and informing trajectory re-planning. The approach reduces the computational burden of repeated optimization while providing provable reachable-set bounds, with potential extensions to disturbances and reachability-based controller design.

Abstract

Control Barrier Functions (CBFs) have been widely utilized in the design of optimization-based controllers and filters for dynamical systems to ensure forward invariance of a given set of safe states. While CBF-based controllers offer safety guarantees, they can compromise the performance of the system, leading to undesirable behaviors such as unbounded trajectories and emergence of locally stable spurious equilibria. Computing reachable sets for systems with CBF-based controllers is an effective approach for runtime performance and stability verification, and can potentially serve as a tool for trajectory re-planning. In this paper, we propose a computationally efficient interval reachability method for performance verification of systems with optimization-based controllers by: (i) approximating the optimization-based controller by a pre-trained neural network to avoid solving optimization problems repeatedly, and (ii) using mixed monotone theory to construct an embedding system that leverages state-of-the-art neural network verification algorithms for bounding the output of the neural network. Results in terms of closeness of solutions of trajectories of the system with the optimization-based controller and the neural network are derived. Using a single trajectory of the embedding system along with our closeness of solutions result, we obtain an over-approximation of the reachable set of the system with optimization-based controllers. Numerical results are presented to corroborate the technical findings.

Neural Network-assisted Interval Reachability for Systems with Control Barrier Function-Based Safe Controllers

TL;DR

The paper tackles runtime verification of safety-critical systems governed by control barrier functions (CBFs), where optimization-based safety filters can induce undesirable behaviors. It introduces a neural network–assisted interval reachability framework that replaces online optimization with a pre-trained neural network approximating the optimal input , and then embeds the NN-controlled system using inclusion functions to obtain interval bounds via mixed-monotone theory; a trajectory of the embedding system yields a hyper-rectangular over-approximation of the reachable set, which is further enlarged by a Minkowski-sum bound to account for approximation error. A key closeness result provides an explicit bound on the trajectory deviation between the true system and the NN-approximated system, enabling rigorous over-approximation of . The method is demonstrated numerically on integrator and double-integrator scenarios with obstacles, showing efficient computation times and accurate containment of true trajectories, thus enabling real-time safety and performance verification and informing trajectory re-planning. The approach reduces the computational burden of repeated optimization while providing provable reachable-set bounds, with potential extensions to disturbances and reachability-based controller design.

Abstract

Control Barrier Functions (CBFs) have been widely utilized in the design of optimization-based controllers and filters for dynamical systems to ensure forward invariance of a given set of safe states. While CBF-based controllers offer safety guarantees, they can compromise the performance of the system, leading to undesirable behaviors such as unbounded trajectories and emergence of locally stable spurious equilibria. Computing reachable sets for systems with CBF-based controllers is an effective approach for runtime performance and stability verification, and can potentially serve as a tool for trajectory re-planning. In this paper, we propose a computationally efficient interval reachability method for performance verification of systems with optimization-based controllers by: (i) approximating the optimization-based controller by a pre-trained neural network to avoid solving optimization problems repeatedly, and (ii) using mixed monotone theory to construct an embedding system that leverages state-of-the-art neural network verification algorithms for bounding the output of the neural network. Results in terms of closeness of solutions of trajectories of the system with the optimization-based controller and the neural network are derived. Using a single trajectory of the embedding system along with our closeness of solutions result, we obtain an over-approximation of the reachable set of the system with optimization-based controllers. Numerical results are presented to corroborate the technical findings.

Paper Structure

This paper contains 9 sections, 2 theorems, 16 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Preliminaries and Problem Statement
  3. Notation and Definitions
  4. Main setup and problem statement
  5. Reachability via Neural Networks and Mixed-monotonicity
  6. Main framework
  7. Closeness of solutions and over-approximation of the reachable sets
  8. Numerical Experiments
  9. Conclusions

Key Result

theorem 1

Consider the filtered system eq:general-system-1 and its approximation eq:general-system-N with the FNN $\mathcal{N}(x)$ satisfying Assumption eq:nnclose. Suppose that $t\mapsto \left[\right]$ is a curve such that $\mathcal{R}_{\texttt{nn}}(t,\mathcal{X}_0)\subseteq [\underline{x}_{\texttt{nn}}(t),\ where $\ell = \sup_{x\in \mathcal{C}} \|g(x)\|_i$ and $\|\cdot\|_i$ is induced norm from $\|\cdot\|

Figures (3)

  • Figure 1: (Left) Trajectories of \ref{['eq:general-system-1']} in Scenario 1. (Right) System \ref{['eq:general-system-N']} with the FNN approximation, and hyper-rectangles $[\underline{x}_{\texttt{nn}}(t), \overline{x}_{\texttt{nn}}(t)]$ starting from several initial sets $[\underline{x}_{\texttt{nn}}(0), \overline{x}_{\texttt{nn}}(0)]$.
  • Figure 2: (Left) Over-approximations $[\underline{x}_{\texttt{nn}}(t), \overline{x}_{\texttt{nn}}(t)]$ and $[\underline{x}_{\texttt{nn}}(t), \overline{x}_{\texttt{nn}}(t)] \oplus \mathcal{B}(r_t,0)$ of the reachable sets, for different initial sets, over $T = 10$ seconds. (Right) As expected, trajectories of the filtered system \ref{['eq:general-system-1']} are contained in $[\underline{x}_{\texttt{nn}}(t), \overline{x}_{\texttt{nn}}(t)] \oplus \mathcal{B}_{\infty}(r_t,0)$.
  • Figure 3: Trajectories of \ref{['eq:general-system-1']} in Scenario 2, hyper-rectangles $[\underline{x}_{\texttt{nn}}(t), \overline{x}_{\texttt{nn}}(t)]$, and over-approximations $[\underline{x}_{\texttt{nn}}(t), \overline{x}_{\texttt{nn}}(t)] \oplus \mathcal{B}_{\infty}(r_t,0)$ of reachable sets, for different initial sets.

Theorems & Definitions (4)

  • theorem 1: Closedness of solutions
  • proof
  • theorem 2: Minkoswki Sum
  • proof