Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Hybrid Zonotope-Based Backward Reachability Analysis for Neural Feedback Systems With Nonlinear Plant Models

Hang Zhang, Yuhao Zhang, Xiangru Xu

TL;DR

This work introduces a novel approach employing hybrid zonotopes to compute the over-approximation of backward reachable sets for neural feedback systems with non-linear plant models and general activation functions.

Abstract

The increasing prevalence of neural networks in safety-critical control systems underscores the imperative need for rigorous methods to ensure the reliability and safety of these systems. This work introduces a novel approach employing hybrid zonotopes to compute the over-approximation of backward reachable sets for neural feedback systems with nonlinear plant models and general activation functions. Closed-form expressions as hybrid zonotopes are provided for the over-approximated backward reachable sets, and a refinement procedure is proposed to alleviate the potential conservatism of the approximation. Two numerical examples are provided to illustrate the effectiveness of the proposed approach.

Hybrid Zonotope-Based Backward Reachability Analysis for Neural Feedback Systems With Nonlinear Plant Models

TL;DR

This work introduces a novel approach employing hybrid zonotopes to compute the over-approximation of backward reachable sets for neural feedback systems with non-linear plant models and general activation functions.

Abstract

The increasing prevalence of neural networks in safety-critical control systems underscores the imperative need for rigorous methods to ensure the reliability and safety of these systems. This work introduces a novel approach employing hybrid zonotopes to compute the over-approximation of backward reachable sets for neural feedback systems with nonlinear plant models and general activation functions. Closed-form expressions as hybrid zonotopes are provided for the over-approximated backward reachable sets, and a refinement procedure is proposed to alleviate the potential conservatism of the approximation. Two numerical examples are provided to illustrate the effectiveness of the proposed approach.
Paper Structure (13 sections, 38 equations, 4 figures, 1 algorithm)

This paper contains 13 sections, 38 equations, 4 figures, 1 algorithm.

Table of Contents

  1. Introduction
  2. Preliminaries & Problem Statement
  3. Hybrid Zonotopes
  4. Problem Statement
  5. Backward Reachability Analysis of ReLU Activated Neural Feedback Systems
  6. Envelope of Nonlinear Functions
  7. Over-approximation of One-step BRS
  8. Refinement of Over-approximated Multi-step BRS
  9. Neural Feedback System With General Types of Activation Functions
  10. Piecewise Linear Activation Functions
  11. Non-Piecewise Linear Activation Functions
  12. Simulation Results
  13. Conclusion

Figures (4)

  • Figure 1: Comparison between OVERT and SOS. Both over-approximate $\tanh(x)$ for $x \in [\![ -\pi/2, \pi/2]\!]$ with the union of 4 polytopes.
  • Figure 2: Over-approximated BRSs without refinement (cyan), the refined over-approximated BRSs (dark green), and samples (red) from the true BRSs for Example \ref{['eg:relu_duffing']}.
  • Figure 3: Comparison of the SOS and OVERT approximation methods at each refinement epoch $n_r$ for Example \ref{['eg:relu_duffing']}.
  • Figure 4: Over-approximation of BRSs for Example \ref{['eg:tanh_duffing']}. The approximation error cannot be further reduced when $n_r > 1$.

Theorems & Definitions (5)

  • proof
  • proof
  • proof
  • proof
  • proof