In this paper, we propose a computationally efficient framework for interval reachability of systems with neural network controllers. Our approach leverages inclusion functions for the open-loop system and the neural network controller to embed the closed-loop system into a larger-dimensional embedding system, where a single trajectory over-approximates the original system's behavior under uncertainty. We propose two methods for constructing closed-loop embedding systems, which account for the interactions between the system and the controller in different ways. The interconnection-based approach considers the worst-case evolution of each coordinate separately by substituting the neural network inclusion function into the open-loop inclusion function. The interaction-based approach uses novel Jacobian-based inclusion functions to capture the first-order interactions between the open-loop system and the controller by leveraging state-of-the-art neural network verifiers. Finally, we implement our approach in a Python framework called ReachMM to demonstrate its efficiency and scalability on benchmarks and examples ranging to $200$ state dimensions.

翻译：本文提出了一种计算高效的神经网络控制器系统区间可达性分析框架。我们的方法利用开环系统和神经网络控制器的包含函数，将闭环系统嵌入到更高维的嵌入系统中，使得单条轨迹能够在不确定性条件下对原始系统行为进行过近似。我们提出了两种构建闭环嵌入系统的方法，分别以不同方式处理系统与控制器之间的交互作用：基于互联的方法通过将神经网络包含函数代入开环包含函数，分别考虑各坐标分量的最坏情况演化；基于交互的方法则利用先进的神经网络验证器，采用新型基于雅可比矩阵的包含函数来捕捉开环系统与控制器之间的一阶交互效应。最后，我们在名为ReachMM的Python框架中实现了所提方法，并在维度高达$200$状态的基准测试和案例中验证了其高效性与可扩展性。