$k$-Inductive and Interpolation-Inspired Barrier Certificates for Stochastic Dynamical Systems

TL;DR

This paper tackles safety verification for discrete-time stochastic dynamical systems by moving beyond single-function barrier certificates to interpolation-inspired barrier certificates (IBC) and k-inductive interpolation-inspired barrier certificates (k-IBC). It shows how a collection of functions, coupled with interpolation and/or k-induction, can relax the classical supermartingale constraint and admit simpler polynomial templates, while still delivering tighter lower bounds on safety probabilities via SOS-based synthesis for polynomial dynamics. The proposed framework encompasses two concrete k-IBC instantiations and two SOS-based synthesis variants, demonstrating improved guarantees on two case studies: a 2D Lotka–Volterra-type model and a 4D system, with reported safety probabilities approaching 0.9997. The work provides a flexible, scalable pathway to certifiable safety that generalizes standard barrier certificates and invites data-driven and neural approaches to certificate discovery and controller synthesis.

Abstract

In this paper, we introduce two new types of barrier certificates that are based on multiple functions rather than a single one. A conventional barrier certificate for a stochastic dynamical system is a nonnegative real-valued function whose expected value does not increase as the system evolves. This requirement guarantees that the barrier certificate forms a nonnegative supermartingale and can be used to derive a lower bound on the probability that the system remains safe. A key advantage of such certificates is that they can be automatically searched for using tools such as optimization programs instantiated with a fixed template. When this search is unsuccessful, the common practice is to modify the template and attempt the synthesis again. Drawing inspiration from logical interpolation, we first propose an alternative framework that uses a collection of functions to jointly serve as a barrier certificate. We refer to this construct as an interpolation-inspired barrier certificate. Nonetheless, we observe that these certificates still require one function in the collection to satisfy a supermartingale condition. Motivated by recent work in the literature, we next combine k-induction with interpolation-inspired certificates to relax this supermartingale constraint. We develop a general and more flexible notion of barrier certificates, which we call k-inductive interpolation-inspired barrier certificates. This formulation encompasses multiple ways of integrating interpolation-inspired barrier certificates with k-induction. We highlight two specific instantiations among these possible combinations. For polynomial systems, we employ sum-of-squares (SOS) programming to synthesize the corresponding set of functions. Finally, through our case studies, we show that the proposed methods enable the use of simpler templates and yield tighter lower bounds on the safety probability.

Figures (6)

• Figure 1: IBC with $\ell = 1$. The purple (overlapping green) and orange shaded regions represent the sets $\{x: 0\leq \mathcal{B}_0(x)\leq \gamma\}$ and $\{x: 0\leq \mathcal{B}_1(x)<1\}$, respectively. The green and red dashed horizontal lines indicate $\gamma$ and $1$, respectively.
• Figure 2: $k$-IBC v1 with $\ell = 2$, $k = 2$. The purple (overlapping green) and orange shaded regions represent the sets $\{x: 0\leq \mathcal{B}_0(x)\leq \gamma\}$ and $\bigcup_{i=1}^{2}\{x: 0\leq \mathcal{B}_i(x) < 1\}$, respectively. The green and red dashed horizontal lines indicate $\gamma$ and $1$, respectively.
• Figure 3: IBC with $\ell = 1$ for Lotka-Volterra type model. The axes show the state variables $v$ and $p$. The blue and purple shaded regions show the sets $\{x: 0\leq \mathcal{B}_0(v,p)\leq \gamma\}$ and $\{x: 0\leq \mathcal{B}_1(v,p)<1\}$, respectively.
• Figure 4: Diagram of an IBC for a nonstochastic system. As each function serves as an overapproximation, there may be overlaps. The union of all the functions gives the inductive invariant set.
• Figure 5: Diagram of a single-function $k$-BC for a nonstochastic system. Every $k$ steps, the trajectory ends in the zero-sublevel set of the certificate.

Theorems & Definitions (25)

• Definition 2.1
• Definition 2.2: Reachability
• Definition 2.4: Safety Probability
• Definition 2.5: Barrier Certificate
• Theorem 2.6: Barrier certificates imply safety prajna2007framework
• Example 1: label=ex1
• Definition 3.1: IBC
• Theorem 3.2: IBCs imply safety
• proof
• Example 2: continues=ex1