k-Inductive Neural Barrier Certificates for Unknown Nonlinear Dynamics

TL;DR

This paper introduces k-inductive neural barrier certificates for safety verification of unknown nonlinear systems, combining neural networks, data-driven modeling, and formal verification techniques.

Contribution

It develops a novel data-driven framework using Willems' lemma and CEGIS-SMT to verify k-inductive neural barrier certificates without requiring explicit system models.

Findings

Successfully verified safety on three nonlinear case studies with unknown dynamics.

Demonstrated the flexibility of the approach by removing restrictions on barrier certificate function classes.

Extended the applicability of neural barrier certificates to partially unknown systems.

Abstract

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 $\epsilon$ -- 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.