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

We introduce two notions of barrier certificates that use multiple functions to provide a lower bound on the probabilistic satisfaction of safety for stochastic dynamical systems. A barrier certificate for a stochastic dynamical system acts as a nonnegative supermartingale, and provides a lower bound on the probability that the system is safe. The promise of such certificates is that their search can be effectively automated. Typically, one may use optimization or SMT solvers to find such barrier certificates of a given fixed template. When such approaches fail, a typical approach is to instead change the template. We propose an alternative approach that we dub interpolation-inspired barrier certificates. An interpolation-inspired barrier certificate consists of a set of functions that jointly provide a lower bound on the probability of satisfying safety. We show how one may find such certificates of a fixed template, even when we fail to find standard barrier certificates of the same template. However, we note that such certificates still need to ensure a supermartingale guarantee for one function in the set. To address this challenge, we consider the use of k-induction with these interpolation-inspired certificates. The recent use of k-induction in barrier certificates allows one to relax the supermartingale requirement at every time step to a combination of a supermartingale requirement every k steps and a c-martingale requirement for the intermediate steps. We provide a generic formulation of a barrier certificate that we dub k-inductive interpolation-inspired barrier certificate. The formulation allows for several combinations of interpolation and k-induction for barrier certificate. We present two examples among the possible combinations. We finally present sum-of-squares programming to synthesize this set of functions and demonstrate their utility in case studies.