Formal Reachability and Robust Stability Analysis of Neural Network Control Systems

Neural networks are increasingly integrated into the closed-loop architecture of modern autonomous and robotic systems, where they are used to represent control policies, perception modules, or components of system models. While such neural network–enabled systems have demonstrated strong empirical performance in complex and uncertain environments, neural networks are known to be highly sensitive to small input perturbations. When embedded in feedback loops, this sensitivity can lead to significant deviations in system behavior, posing serious challenges for safety-critical applications. These challenges highlight the need for rigorous, formal analysis tools capable of characterizing and certifying the behavior of neural network control systems. This dissertation addresses this need by developing systematic and theoretically grounded methods for analyzing and certifying key properties of neural network control systems.

The first part of this dissertation addresses the reachability analysis of neural networks using set-based computational methods. This dissertation presents the first systematic application of hybrid zonotopes to the reachability analysis of neural networks, employing them as a unified and expressive set representation for computing both forward and backward reachable sets. By exploiting the structural properties of neural networks, the proposed methods enable exact or provably over-approximated representations of the neural network input–output mapping, allowing reachable sets to be efficiently computed through set-propagation operations. To overcome the scalability challenges associated with large neural networks, this dissertation further introduces tunable and computationally efficient network reduction and abstraction techniques that provide a flexible trade-off between approximation accuracy and computational complexity.

The second part of this dissertation studies the hybrid-zonotopes-based reachability analysis and safety verification of neural network control systems by building upon the results developed in the first part. Both the neural network controller and the plant dynamics are represented using hybrid zonotopes, enabling their interconnection to be encoded through simple hybrid-zonotope set operations. Consequently, when the initial and target sets of the neural network control system are expressed as hybrid zonotopes, the corresponding forward and backward reachable sets can also be constructed within the same representation framework. Based on the computed reachable sets, safety verification problems are formulated as mixed-integer linear programs, enabling sound and, in certain cases, complete safety certification for neural network control systems.

The third part of this dissertation investigates the robust stability properties of neural network control systems, with particular emphasis on robustness in the presence of modeling uncertainties. By integrating classical Lyapunov stability theory with quadratic constraint–based abstractions of neural networks, we derive novel robust stability certificates for neural network control systems with interval matrix uncertainties, formulated as linear matrix inequalities. To mitigate the associated computational burden, three relaxed sufficient conditions are developed, and their equivalence in terms of feasibility is rigorously established. The proposed stability framework is further extended to a data-driven setting, where explicit system models are unavailable but input–state observations of system behavior are accessible. Collectively, these results establish a rigorous framework for the stability verification of neural network control systems.