Vector Certificates for $\omega$-regular Specifications

TL;DR

This paper introduces vector certificates, a new approach using multiple functions to verify $0$-regular properties in dynamical systems, overcoming limitations of single-function templates.

Contribution

It proposes vector co-Bdchi ranking functions and closure certificates, extending existing certificates to jointly overapproximate invariants, enabling verification when single-function methods fail.

Findings

Successfully verified $0$-regular properties in case studies.

Demonstrated effectiveness of SOS programming for vector certificates.

Provided a method to handle cases where fixed templates are insufficient.

Abstract

The recently introduced notions of ranking functions and closure certificates utilize well-foundedness arguments to facilitate the verification of dynamical systems against $\omega$-regular properties. A ranking function and a closure certificate are real-valued functions defined over states and state pairs of a dynamical system whose zero superlevel sets are inductive state invariant and inductive transition invariant, respectively. The search for such certificates can be automated by fixing a specific template class, such as a polynomial of a fixed degree, and then using optimization techniques such as sum-of-squares (SOS) programming to find it. Unfortunately, such certificates may not be found for a fixed template. In such a case, one must change the template; for example, increase the degree of the polynomial. In this paper, we consider a notion of multiple functions in the form of vector certificates. Taking inspiration from the literature on vector barrier certificates as generalizations of standard barrier certificates for safety verification, we propose vector co-B\"uchi ranking functions and vector closure certificates as nontrivial generalizations of ranking functions and closure certificates, respectively. Both notions consist of a set of functions that jointly overapproximate an inductive invariant by considering each function to be a linear combination of the others. The advantage of such 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 an SOS programming approach to search for these functions and demonstrate the effectiveness of our proposed method in verifying $\omega$-regular specifications in several case studies.