Interpolation-Inspired Closure Certificates

TL;DR

This paper introduces interpolation-inspired closure certificates, a new approach for verifying dynamical systems' safety properties by using multiple functions to over-approximate transition invariants, enhancing the ability to prove complex properties.

Contribution

It proposes a novel set of closure certificates that combine multiple functions to verify invariants, overcoming limitations of fixed-template methods.

Findings

Effective verification of $oldsymbol{ ext{ω}}$-regular properties demonstrated.

SOS programming and scenario approach successfully used to find closure sets.

Method outperforms traditional single-function certificates in case studies.

Abstract

Barrier certificates, a form of state invariants, provide an automated approach to the verification of the safety of dynamical systems. Similarly to barrier certificates, recent works explore the notion of closure certificates, a form of transition invariants, to verify dynamical systems against $\omega$-regular properties including safety. A closure certificate, defined over state pairs of a dynamical system, is a real-valued function whose zero superlevel set characterizes an inductive transition invariant of the system. The search for such a certificate can be effectively automated by assuming it to be within a specific template class, e.g. a polynomial of a fixed degree, and then using optimization techniques such as sum-of-squares (SOS) programming to find it. Unfortunately, one may not be able to find such a certificate for a fixed template. In such a case, one must change the template, e.g. increase the degree of the polynomial. In this paper, we consider a notion of multiple closure certificates dubbed interpolation-inspired closure certificates. An interpolation-inspired closure certificate consists of a set of functions which jointly over-approximate a transition invariant by first considering one-step transitions, then two, and so on until a transition invariant is obtained. The advantage of interpolation-inspired closure certificates is that they allow us to prove properties even when a single function for a fixed template cannot be found using standard approaches. We present SOS programming and a scenario program to find these sets of functions and demonstrate the effectiveness of our proposed method to verify persistence and general $\omega$-regular specifications in some case studies.