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.

翻译：传统（k=1）离散时间屏障证书条件通过要求函数在每一步非增而施加严格安全约束，而k-归纳屏障证书通过允许临时增加（最多k-1次，每次在阈值$ε$内）来放松这一约束，在保持整体安全性的同时提升灵活性。本文利用神经网络，为（部分）未知非线性系统构建k-归纳神经屏障证书（k-NBCs）。虽然神经网络在设计过程中具有可扩展性，但缺乏形式化保证，需要借助额外方法（如结合可满足性模理论（SMT）的反例引导归纳合成（CEGIS））进行验证。然而，CEGIS-SMT框架需要系统动力学知识，而这在实际场景中难以获得。为此，我们利用Willems等人基本引理的泛化形式，通过单一状态轨迹构建（部分）未知模型的数据驱动表示，用于SMT验证且不损失精度。此外，CEGIS-SMT进一步消除了将屏障证书限制为特定函数类（如平方和函数）的约束，从而提供了更大的设计灵活性。我们在三个具有（部分）未知动力学的非线性案例研究中验证了所提出方法。