Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Online Data-Driven Safety Certification for Systems Subject to Unknown Disturbances

Nicholas Rober, Karan Mahesh, Tyler M. Paine, Max L. Greene, Steven Lee, Sildomar T. Monteiro, Michael R. Benjamin, Jonathan P. How

TL;DR

This paper tackles runtime safety verification for autonomous systems subject to unknown disturbances by introducing an online, data-driven safety-certification framework that fuses moving-horizon estimation (MHE) with forward reachability analysis encoded as a computational-graph relaxation. Disturbances and their statistics are estimated online with MHE, and the nominal dynamics plus disturbance bias are propagated through a CG relaxation to produce reachable-set over-approximations (RSOAs) that can be checked against unsafe and goal regions in real time. A formal guarantee (via an online safety-certification result) accompanies the RSOAs, and the method is validated on hardware with a 6-DOF unmanned surface vehicle, achieving real-time reachability at 10 Hz under currents and actuator faults. The combination of data-driven disturbance estimation, CG-based bound propagation, and real-time applicability advances practical safety assurances for complex, uncertain robotic systems while maintaining computational tractability.

Abstract

Deploying autonomous systems in safety critical settings necessitates methods to verify their safety properties. This is challenging because real-world systems may be subject to disturbances that affect their performance, but are unknown a priori. This work develops a safety-verification strategy wherein data is collected online and incorporated into a reachability analysis approach to check in real-time that the system avoids dangerous regions of the state space. Specifically, we employ an optimization-based moving horizon estimator (MHE) to characterize the disturbance affecting the system, which is incorporated into an online reachability calculation. Reachable sets are calculated using a computational graph analysis tool to predict the possible future states of the system and verify that they satisfy safety constraints. We include theoretical arguments proving our approach generates reachable sets that bound the future states of the system, as well as numerical results demonstrating how it can be used for safety verification. Finally, we present results from hardware experiments demonstrating our approach's ability to perform online reachability calculations for an unmanned surface vehicle subject to currents and actuator failures.

Online Data-Driven Safety Certification for Systems Subject to Unknown Disturbances

TL;DR

This paper tackles runtime safety verification for autonomous systems subject to unknown disturbances by introducing an online, data-driven safety-certification framework that fuses moving-horizon estimation (MHE) with forward reachability analysis encoded as a computational-graph relaxation. Disturbances and their statistics are estimated online with MHE, and the nominal dynamics plus disturbance bias are propagated through a CG relaxation to produce reachable-set over-approximations (RSOAs) that can be checked against unsafe and goal regions in real time. A formal guarantee (via an online safety-certification result) accompanies the RSOAs, and the method is validated on hardware with a 6-DOF unmanned surface vehicle, achieving real-time reachability at 10 Hz under currents and actuator faults. The combination of data-driven disturbance estimation, CG-based bound propagation, and real-time applicability advances practical safety assurances for complex, uncertain robotic systems while maintaining computational tractability.

Abstract

Deploying autonomous systems in safety critical settings necessitates methods to verify their safety properties. This is challenging because real-world systems may be subject to disturbances that affect their performance, but are unknown a priori. This work develops a safety-verification strategy wherein data is collected online and incorporated into a reachability analysis approach to check in real-time that the system avoids dangerous regions of the state space. Specifically, we employ an optimization-based moving horizon estimator (MHE) to characterize the disturbance affecting the system, which is incorporated into an online reachability calculation. Reachable sets are calculated using a computational graph analysis tool to predict the possible future states of the system and verify that they satisfy safety constraints. We include theoretical arguments proving our approach generates reachable sets that bound the future states of the system, as well as numerical results demonstrating how it can be used for safety verification. Finally, we present results from hardware experiments demonstrating our approach's ability to perform online reachability calculations for an unmanned surface vehicle subject to currents and actuator failures.
Paper Structure (10 sections, 2 theorems, 12 equations, 2 figures, 1 algorithm)

This paper contains 10 sections, 2 theorems, 12 equations, 2 figures, 1 algorithm.

Table of Contents

  1. Introduction
  2. Related Work
  3. Preliminaries
  4. System Dynamics
  5. Reachability Analysis
  6. Computational Graphs
  7. Computational Graph Relaxation
  8. Moving-Horizon Estimation
  9. Reachability for Uncertain Systems
  10. Conclusion

Key Result

Theorem III.1

Given a CG $\bm{G}$ and a hyper-rectangular set of possible inputs $\mathcal{I}$, there exist two explicit functions such that the inequality $g^{\bm{G}}_{L,o}(\mathbf{z}) \leq g^{\bm{G}}_o(\mathbf{z}) \leq g^{\bm{G}}_{U,o}(\mathbf{z})$ holds element-wise for all $\mathbf{z} \in \mathcal{I}$, with $\bm{\Psi}, \bm{\Phi} \in \mathbb{R}^{n_o \times n_i}$ and $\bm{\alpha}, \bm{\beta} \in \mathbb{R}^{

Figures (2)

  • Figure 1: Reachability analysis detects a possible collision for a system experiencing a hardware malfunction
  • Figure 2: Block diagram depicting our approach. Data is collected from the system and fed into the MHE, which estimates the state and disturbance terms. The outputs of the MHE are used with a CG representation of the closed-loop dynamics to conduct reachability analysis and certify safety.

Theorems & Definitions (3)

  • Theorem III.1: Linear Relaxation of CGs xu2020automatic
  • Theorem IV.1: Safety Verification for an Uncertain System
  • proof