Co-Buchi Barrier Certificates for Discrete-time Dynamical Systems

TL;DR

The paper addresses automata-based safety verification for discrete-time dynamical systems by introducing Co-Büchi barrier certificates (CBBCs), which certify that a region is visited only finitely often. The core idea is to augment the system state with a counter and define a co-Büchi safety condition that bounds region visits by a parameter $k$, enabling verification against universal co-Büchi automata through a product construction. The authors present two computational frameworks—SOS-based and SMT-based (CEGIS)—to search for CBBCs, and prove that CBBCs generalize the prior state-triplet approach, including a constructive subsumption argument. Case studies on a room-temperature model, a 2D Van der Pol oscillator, and a 3D Kuramoto oscillator demonstrate the practicality and scalability of CBBCs, with certificates provided or referenced in appendices. The work offers a new, safety-centric lens for ω-regular verification in continuous-space dynamics and points to future work on synthesis and extensions to stochastic and timed settings.

Abstract

Barrier certificates provide functional overapproximations for the reachable set of dynamical systems and provide inductive guarantees on the safe evolution of the system. In automata-theoretic verification, a key query is to determine whether the system visits a given predicate over the states finitely often, typically resulting from the complement of the traditional Buchi acceptance condition. This paper proposes a barrier certificate approach to answer such queries by developing a notion of co-Buchi barrier certificates (CBBCs) that generalize classic barrier certificates to ensure that the traces of a system visit a given predicate a fixed number of times. Our notion of CBBC is inspired from bounded synthesis paradigm to LTL realizability, where the LTL specifications are converted to safety automata via universal co-Buchi automata with a bound on final state visitations provided as a hyperparameter. Our application of CBBCs in verification is analogous: we fix a bound and search for a suitable barrier certificate, increasing the bound if no suitable function can be found. We then use these CBBCs to verify our system against properties specified by co-Buchi automata and demonstrate their effectiveness via some case studies.

Figures (6)

• Figure 1: Example NBA $\mathcal{A}_{b_1}$ from Section \ref{['sec:intro']} which represents the complement of a safety specification.
• Figure 2: Automaton $\mathcal{A}'_{b_1}$ created from unfolding NBA $\mathcal{A}_b$ in Section \ref{['sec:intro']} (Figure \ref{['fig:aut_eg_1']}).
• Figure 3: UCA $\mathcal{A}_c$ for Subsection \ref{['subsec:case_study_triplet']}.
• Figure 4: UCA $\mathcal{A}_c$ for Subsection \ref{['subsec:case_study_osc']}.
• Figure 5: Corner cases where multiple barrier certificates are present for the same intermediate state. In all cases we can reduce this to a single barrier certificate over the state $q'$. Here we can either replace the barrier certificates with the maximum or minimum or ignore these.

Theorems & Definitions (16)

• Definition 2.1
• Theorem 2.2
• Lemma 2.3
• proof
• Corollary 2.5
• Definition 3.1
• Theorem 3.2
• proof
• Lemma 3.3
• proof