Counterexample-Guided Inductive Synthesis (CEGIS)

k-Inductive Neural Barrier Certificates for Unknown Nonlinear Dynamics

This paper introduces k-inductive neural barrier certificates (k-NBCs) for safety verification of partially unknown nonlinear dynamical systems. The approach relaxes strict conventional barrier conditions by allowing temporary function increases up to k-1 times, and combines neural networks with a CEGIS-SMT verification framework. To handle unknown dynamics, it leverages a data-driven representation via Willems et al.'s fundamental lemma from a single state trajectory, avoiding the need for explicit system models. The method is validated on three nonlinear case studies.