Co-Buchi Barrier Certificates for Discrete-time Dynamical Systems

TL;DR

This paper introduces co-Buchi barrier certificates (CBBCs), a novel method for verifying discrete-time dynamical systems against properties that require visiting certain states finitely often, extending traditional barrier certificates.

Contribution

The paper develops co-Buchi barrier certificates (CBBCs) that generalize classic barrier certificates to handle finiteness constraints in system traces, inspired by bounded synthesis in automata theory.

Findings

CBBCs effectively verify systems against co-Buchi automata properties.

The approach generalizes barrier certificates to finiteness constraints.

Case studies demonstrate practical applicability and effectiveness.

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.