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.

本研究提出了一种计算效率高的方法，用于神经网络控制系统的区间可达性问题。通过引入包含函数来构建神经网络控制器和开环系统，并基于函数雅各比矩阵的边界介绍并分析了一类适用于捕获系统和神经网络控制器之间相互作用的开环动力学的包含函数。基于包含函数，构建了一个比原系统状态数多两倍的嵌入系统，并证明该嵌入系统的单一轨迹提供了可达集的超矩形过估计。最后，通过两种不同的方式构建了一个闭环嵌入系统，以考虑系统和控制器之间的交互作用。实验证明了本方法在现有基准测试中优于已有方法，同时在一个包含多达200个状态的车队编组示例中显示了可扩展性。

神经网络反馈循环的高效交互感知区间分析