Learning k-Inductive Control Barrier Certificates for Unknown Nonlinear Dynamics Beyond Polynomials

This work is concerned with synthesizing safety controllers for discrete-time nonlinear systems beyond polynomials with unknown mathematical models using the notion of k-inductive control barrier certificates (k-CBCs). Conventional CBC conditions (with k=1) for ensuring safety over dynamical systems are often restrictive, as they require the CBCs to be non-increasing at every time step. Inspired by the success of k-induction in software verification, k-CBCs relax this requirement by allowing the barrier function to be non-increasing over k steps, while permitting k-1 (one-step) increases, each up to a threshold epsilon. This relaxation enhances the likelihood of finding feasible k-CBCs while providing safety guarantees across the dynamical systems. Despite showing promise, existing approaches for constructing k-CBCs often rely on precise mathematical knowledge of system dynamics, which is frequently unavailable in practical scenarios. In this work, we address the case where the underlying dynamics are unknown, a common occurrence in real-world applications, and employ the concept of persistency of excitation, grounded in Willems et al.'s fundamental lemma. This result implies that input-output data from a single trajectory can capture the behavior of an unknown system, provided the collected data fulfills a specific rank condition. We employ sum-of-squares (SOS) programming to synthesize the k-CBC as well as the safety controller directly from data while ensuring the safe behavior of the unknown system. The efficacy of our approach is demonstrated through a set of physical benchmarks with unknown dynamics, including a DC motor, an RLC circuit, a nonlinear nonpolynomial car, and a nonlinear polynomial Lorenz attractor.