$k$-Inductive and Interpolation-Inspired Barrier Certificates for Stochastic Dynamical Systems
About
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.