Guaranteed-Safe Approximate Reachability via State Dependency-Based Decomposition

TL;DR

This paper introduces a novel state dependency graph approach to decompose complex dynamical systems, enabling fast and guaranteed-safe approximation of backward reachable tubes for high-dimensional robotic systems.

Contribution

It proposes a new decomposition method using state dependency graphs that preserves safety guarantees while reducing computational complexity for high-dimensional systems.

Findings

Efficient approximation of BRTs for 4D and 6D systems

Preserves safety guarantees in decomposed subsystems

Enables analysis of previously intractable high-dimensional models

Abstract

Hamilton Jacobi (HJ) Reachability is a formal verification tool widely used in robotic safety analysis. Given a target set as unsafe states, a dynamical system is guaranteed not to enter the target under the worst-case disturbance if it avoids the Backward Reachable Tube (BRT). However, computing BRTs suffers from exponential computational time and space complexity with respect to the state dimension. Previously, system decomposition and projection techniques have been investigated, but the trade off between applicability to a wider class of dynamics and degree of conservatism has been challenging. In this paper, we propose a State Dependency Graph to represent the system dynamics, and decompose the full system where only dependent states are included in each subsystem, and "missing" states are treated as bounded disturbance. Thus for a large variety of dynamics in robotics, BRTs can be quickly approximated in lower-dimensional chained subsystems with the guaranteed-safety property preserved. We demonstrate our method with numerical experiments on the 4D Quadruple Integrator, and the 6D Bicycle, an important car model that was formerly intractable.