神经反馈系统中验证可达-回避规范的新策略
A New Strategy for Verifying Reach-Avoid Specifications in Neural Feedback Systems
AI总结：
本文提出了一种新的算法，用于计算神经反馈系统中可达-回避规范的上界和下界近似值，并结合前向分析技术，构建统一的验证框架。
摘要：
前向可达性分析是验证神经反馈系统（由神经网络控制的动态系统）可达-回避属性的主要方法。这种主导地位源于现有后向可达性方法的可扩展性有限。在本工作中，我们引入了新的算法，用于计算此类系统的后向可达集的上界和下界近似值。我们进一步将这些后向算法与已确立的前向分析技术相结合，从而获得一种统一的神经反馈系统验证框架。
英文摘要：
Forward reachability analysis is the predominant approach for verifying reach-avoid properties in neural feedback systems (dynamical systems controlled by neural networks). This dominance stems from the limited scalability of existing backward reachability methods. In this work, we introduce new algorithms that compute both over- and under-approximations of backward reachable sets for such systems. We further integrate these backward algorithms with established forward analysis techniques to yield a unified verification framework for neural feedback systems.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
