Exact and Efficient Hamilton-Jacobi-based Guaranteed Safety Analysis via System Decomposition

Hamilton-Jacobi (HJ) reachability is a method that provides rigorous analyses of the safety properties of dynamical systems. This method has been successfully applied to many low-dimensional dynamical system models such as coarse models of aircraft and quadrotors in order to provide safety guarantees in potentially dangerous scenarios. These guarantees can be provided by the computation of a backward reachable set (BRS), which represents the set of states from which the system may be driven into violating safety properties despite the system's best effort to remain safe. Unfortunately, HJ reachability is not practical for high-dimensional systems because the complexity of the BRS computation scales exponentially with the number of state dimensions. Although numerous approximation techniques are able to tractably provide conservative estimates of the BRS, they often require restrictive assumptions about system dynamics without providing an exact solution. In this paper we propose a general method for decomposing dynamical systems. Even when the resulting subsystems are coupled, relatively high-dimensional BRSs that were previously intractable or expensive to compute can now be quickly and exactly computed in lower-dimensional subspaces. As a result, the curse of dimensionality is alleviated to a large degree without sacrificing optimality. We demonstrate our theoretical results through two numerical examples: a 3D Dubins Car model and a 6D Acrobatic Quadrotor model.