用神经网络设计可容忍短暂突破的安全验证器,适用于未知非线性系统。
k-Inductive Neural Barrier Certificates for Unknown Nonlinear Dynamics

- 基于k-归纳思想,允许安全函数短期小幅上升,提升灵活性。
- 仅需单条轨迹数据,通过广义Willems引理构建未知模型用于形式验证。
- 结合CEGIS-SMT框架,无需预设函数形式,适合复杂动态系统安全分析。
传统离散时间屏障证书(k=1)要求每一步函数值不增加,约束严格;而k-归纳屏障证书允许最多k-1次、每次不超过ε的临时上升,保持整体安全性的同时提升灵活性。本文提出k-归纳神经屏障证书(k-NBC),用于(部分)未知非线性系统的安全验证。神经网络虽具可扩展性,但缺乏形式保证,需借助反例引导归纳合成(CEGIS)与满足性模理论(SMT)进行验证。然而传统CEGIS-SMT依赖系统动力学知识,实际中难以获取。为此,本文利用Willems等人的基本引理的推广,仅通过一条状态轨迹即可构建(部分)未知系统的数据驱动表示,实现无损精度的SMT验证。此外,该方法摆脱了对特定函数类(如平方和多项式)的限制,使屏障证书设计更灵活。在三个具有(部分)未知动力学的非线性案例上验证了所提方法的有效性。
原文摘要 · Abstract (English)
While conventional (k=1) discrete-time barrier certificate conditions impose strict safety constraints by requiring the function to be non-increasing at every step, k-inductive barrier certificates relax this by allowing a temporary increase -- up to k-1 times, each within a threshold $ε$ -- while maintaining overall safety, and improving flexibility. This paper leverages neural networks and constructs k-inductive neural barrier certificates (k-NBCs) for (partially) unknown nonlinear systems. While neural networks offer scalability in the design process, they lack formal guarantees, requiring additional approaches such as counterexample-guided inductive synthesis (CEGIS) with satisfiability modulo theories (SMT) for verification. However, the CEGIS-SMT framework requires knowledge of system dynamics, which is unavailable in practical settings. To address this, we leverage the generalization of the Willems et al.'s fundamental lemma, using a single state trajectory, to construct a data-driven representation of (partially) unknown models for SMT verification without sacrificing accuracy. Additionally, CEGIS-SMT further removes the constraint of restricting barrier certificates to specific function classes, such as sum-of-squares, enabling greater flexibility in their design. We validate our approach on three nonlinear case studies with (partially) unknown dynamics.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。