Reachability Analysis Using Hybrid Zonotopes and Functional Decomposition

TL;DR

This work tackles scalable reachability analysis for nonlinear systems, including those with neural-network controllers and logic-based components. It develops a unified framework using hybrid zonotopes, state-update sets $\Psi$, and state-input maps $\Theta$, augmented by functional decomposition and SOS-style approximations to linearize memory growth over time and scale linearly with state dimension. Key contributions include identities to enclose nonlinear graphs compatible with hybrid zonotopes, a generalized method to construct open-loop state-update sets and state-input maps, and an efficient vertex-to-hybrid-zonotope conversion with complexity guarantees. The approach is validated on a nonlinear inverted pendulum with NN control, high-dimensional Boolean dynamics, and a Vertical Collision Avoidance System, demonstrating tight over-approximations, improved scalability, and exact or near-exact reachability in challenging hybrid/nonlinear scenarios. The results suggest practical impact for real-time verification and safety guarantees in complex cyber-physical systems.

Abstract

This paper proposes methods for reachability analysis of nonlinear systems in both open loop and closed loop with advanced controllers. The methods combine hybrid zonotopes, a construct called a state-update set, functional decomposition, and special ordered set approximations to enable linear growth in reachable set memory complexity with time and linear scaling in computational complexity with the system dimension. Facilitating this combination are new identities for constructing nonconvex sets that contain nonlinear functions and for efficiently converting a collection of polytopes from vertex representation to hybrid zonotope representation. Benchmark numerical examples from the literature demonstrate the proposed methods and provide comparison to state-of-the-art techniques.

Figures (8)

• Figure 1: The closed-loop successor set identity uses a set-based representation of the closed-loop dynamics, called the closed-loop state-update set $\Phi$, to generate the one-step forward reachable set $\mathcal{R}_{k+1}$ from $\mathcal{R}_{k}$. The closed-loop state-update set is created by combining sets representing the open-loop dynamics and a state-feedback controller, called the open-loop state-update set $\Psi$ and the state-input map $\Theta$, respectively.
• Figure 2: Visual depiction of functional decomposition and Theorem \ref{['thm-FunctionCompSets']} applied to $x_{k+1}=\cos(\pi \sin(x_k))$ with the decomposition shown in Table \ref{['tab:UnaryDecomp']}. Here, $\mathcal{H}_{1:\ell}$ denotes a stage in the recursion of Theorem \ref{['thm-FunctionCompSets']}. $\mathcal{H}_{1:1}$ and $\mathcal{H}_{1:1}\times D_2$ are a line and a rectangle, respectively, and are not shown. (a) The first of two recursions of \ref{['eqn-Hs-Rec']} yields $\mathcal{H}_{1:2}$ (blue). (b) The first step in the second recursion of \ref{['eqn-Hs-Rec']} gives $\mathcal{H}_{1:2}\times D_3$ (also shown in blue). (c) The second step of the second recursion of \ref{['eqn-Hs-Rec']} takes a generalized intersection with $\mathcal{H}_3$ (red) and yields $\mathcal{H}_{1:3}$ (black). (d) Corollary \ref{['co-H_inNout']} eliminates the intermediate variable $w_2$ using a projection and is the last step in producing the state-update set $\Phi$ (magenta). (e-h) Per Corollary \ref{['co-SusOA_ReachOA']}, over-approximation of the functions used for decomposition results in an over-approximation of the state-update set $\bar{\Phi}\supset \Phi$.
• Figure 3: A sinusoid (green) is approximated using an SOS approximation for $x\in[-4,4]$ and represented as a hybrid zonotope (red). Using formal bounds for SOS approximation error, the SOS approximation is bloated in the output dimension to create an enclosure of a sine wave for $x\in[-4,4]$, which is also represented as a hybrid zonotope (blue).
• Figure 4: Comparison of three methods for over-approximating $\{xyxy^T)\ |\ (x,y)\in[-1\ 1]^2\}$.
• Figure 5: (a) Projection of over-approximated open-loop state-update set $\Bar{\Psi}$ bounding dynamics of a pendulum at discrete time steps. (b) State-input map $\Theta$ of a neural network trained to mimic NMPC. (c) Projection of over-approximated closed-loop state-update set found using Theorem \ref{['thm-CLSUSfromOL']} by coupling $\Bar{\Psi}$ and $\Theta$.

Theorems & Definitions (30)

• Definition 1
• Definition 2
• Definition 3
• Definition 4: SOS Approximation
• Example 1
• Remark 1: Affine Decompositions
• Example 2
• Remark 2: Existence of a Functional Decomposition
• Definition 5
• Theorem 1