In this paper, we propose a computationally efficient framework for interval reachability of neural network controlled systems. Our approach builds upon inclusion functions for the neural network controller and the open-loop system. We observe that many state-of-the-art neural network verifiers can produce inclusion functions for neural networks. We introduce and analyze a new class of inclusion functions for the open-loop dynamics based on bounds of the function Jacobian that is particularly suitable for capturing the interactions between systems and neural network controllers. Next, for any dynamical system, we use inclusion functions to construct an embedding system with twice the number of states as the original system. We show that a single trajectory of this embedding system provides hyper-rectangular over-approximations of reachable sets. We then propose two approaches for constructing a closed-loop embedding system for a neural network controlled dynamical system that accounts for the interaction between the system and the controller in different ways. The interconnection-based approach accounts for the worst-case evolution of each coordinate separately by substituting the neural network inclusion function into the open-loop embedding system. The interaction-based approach uses the newly introduced class of Jacobian-based inclusion functions to fully capture first-order interactions between the system and the controller. Finally, we implement our approach in a Python framework called \texttt{ReachMM} and show that on several existing benchmarks, our methods outperform the existing approaches in the literature. We also demonstrate the scalability of our method on a vehicle platooning example with up to $200$ states.

翻译：本文提出了一种计算高效的神经网络控制系统区间可达性分析框架。该方法基于神经网络控制器与开环系统的包含函数。我们注意到，现有多种先进的神经网络验证工具均能生成神经网络的包含函数。针对开环动力学系统，我们引入并分析了一类基于函数雅可比矩阵边界的新型包含函数，该函数特别适用于捕捉系统与神经网络控制器之间的交互作用。随后，对于任意动力学系统，我们利用包含函数构建一个状态数为原系统两倍的嵌入系统，并证明该嵌入系统的单条轨迹即可提供可达集的超矩形过逼近。在此基础上，我们提出两种构建神经网络控制闭环嵌入系统的方法，分别以不同方式考虑系统与控制器之间的交互：基于互联的方法通过将神经网络包含函数代入开环嵌入系统，独立处理每个坐标的最坏情况演化；基于交互的方法则利用新引入的雅可比包含函数，完整捕捉系统与控制器间的一阶交互。最后，我们在Python框架\texttt{ReachMM}中实现所提方法，并在多个基准测试中验证其性能优于现有文献方法。同时，我们通过一个包含$200$个状态的车队跟驰算例展示了该方法良好的可扩展性。