Vector Certificates for $ω$-regular Specifications

TL;DR

This paper proposes vector co-Buchi ranking functions and vector closure certificates as nontrivial generalizations of ranking functions and closure certificates, respectively, and presents an SOS programming approach to search for these functions.

Abstract

The recently introduced notions of ranking functions and closure certificates utilize well-foundedness arguments to facilitate the verification of dynamical systems against $ω$-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üchi 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 $ω$-regular specifications in several case studies.

Figures (4)

• Figure 1: Illustrative example demonstrating the existence of VCCs over barrier certificates. The initial state is shown in green. The unsafe states are shown in red.
• Figure 2: Sampled state trajectories of simple dynamic model. The trajectory lines show jumps. The green and red shaded regions represent $\mathcal{X}_0$ and $\mathcal{X}_u$, respectively. Set $\mathcal{X}_u$ is never visited. Note that as we deal with discrete time systems, the states of the system jump and thus, the trajectories do not intersect with the unsafe region.
• Figure 3: Sampled state trajectories of Van der Pol oscillator model. The green and red shaded regions represent $\mathcal{X}_0$ and $\mathcal{X}_u$, respectively. Set $\mathcal{X}_u$ is never visited.
• Figure 4: A (nondeterministic) Büchi automaton $\mathcal{A}$ for the LTL specification from Section \ref{['subsec:casestudy_ltl']}. The automata represents the LTL formula $\neg( \mathsf{F} \neg a \land \mathsf{F} \neg b \land \mathsf{FG} \neg c)$.

Theorems & Definitions (30)

• Definition 2.1
• Definition 2.2: BC
• Theorem 1: BCs imply safety prajna2004safety
• Definition 2.3: VBC
• Theorem 2: VBCs imply safety sogokon2018vector
• Definition 2.4: CC for Safety
• Theorem 3: CCs imply safety murali2024closure
• Definition 2.5: CC for Persistence
• Theorem 4: CCs imply Persistence murali2024closure
• Definition 2.6: BRF for Recurrence