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

TL;DR

This work addresses safety guarantees for unknown discrete-time dynamical systems by introducing $k$-inductive control barrier certificates ($k$-CBCs) and learning them from a single input-state trajectory. It develops data-driven representations for both linear and nonlinear dynamics, leveraging persistency of excitation (via Willems' lemma) to relate observed data to closed-loop behavior, and formulates sum-of-squares (SOS) programs to synthesize the $k$-CBC and the accompanying safety controller. The approach generalizes conventional CBCs (recovered at $k=1$, $ ext{ε}=0$) and supports nonlinear, nonpolynomial dynamics through an exaggerated dictionary and nonlinearity cancellation when possible. Case studies on an unknown RLC circuit, DC motor, nonpolynomial car, and Lorenz attractor demonstrate that safe operation can be achieved from a single trajectory, with $k>1$ enabling feasible certificates where $k=1$ fails. The work offers a practical, data-driven pathway to formal safety guarantees in settings where exact models are unavailable, with future work extending to continuous-time systems via $t$-barrier certificates.

Abstract

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.

Figures (5)

• Figure 1: A CBC $\mathcal{B}(x)$ for a dynamical system, with the dashed line representing the initial level set $\mathcal{B}(x) = \gamma$. Purple and red circles are initial and unsafe regions, respectively.
• Figure 2: Closed-loop state trajectories of the RLC circuit ($100$ trajectories shown in black) under the designed controller and $k$-CBC with $k=3$, as defined in \ref{['eq:RLC_controller']}. Purple and red boxes are initial and unsafe regions, respectively. The level sets $\gamma$ and $\lambda$ are depicted in blue and dashed black, respectively.
• Figure 3: Closed-loop state trajectories of the DC motor ($100$ trajectories shown in black) under the designed controller and $k$-CBC with $k=3$, as defined in \ref{['eq:DC_controller']}. Purple and red boxes are initial and unsafe regions, respectively. The level sets $\gamma$ and $\lambda$ are depicted in blue and dashed black, respectively.
• Figure 4: Closed-loop state trajectories of the nonpolynomial car ($50$ trajectories shown in black) under the designed controller and $k$-CBC with $k=2$. Emerald green and maroon boxes are initial and unsafe regions, respectively. The level sets $\gamma$ and $\lambda$ are depicted in dark and light gray, respectively.
• Figure 5: Closed-loop state trajectories of the Lorenz system ($50$ trajectories shown in black) under the designed controller and $k$-CBC with $k=2$. Emerald green and maroon boxes are initial and unsafe regions, respectively. The level sets $\gamma$ and $\lambda$ are depicted in dark and light gray, respectively.

Theorems & Definitions (23)

• Definition 2.1
• Definition 2.2: CBC - prajna2004safety
• Definition 2.3: $k$-CBC - Anand2021kSafety
• Theorem 2.4: Anand2021kSafety
• Lemma 3.1
• proof
• Remark 3.2
• Theorem 3.3
• proof
• Definition 4.1