k-Inductive Neural Barrier Certificates for Unknown Nonlinear Dynamics
This work addresses the problem of safety verification for unknown nonlinear systems, offering a more flexible barrier certificate condition that can tolerate temporary increases in the barrier function, which is particularly relevant for data-driven control applications.
This paper introduces k-inductive neural barrier certificates (k-NBCs) for (partially) unknown nonlinear systems, using a data-driven representation based on Willems et al.'s fundamental lemma to enable SMT verification without system dynamics. The approach is validated on three nonlinear case studies, demonstrating improved flexibility over conventional barrier certificates.
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.