Technical Summary: Co-Büchi Barrier Certificates for Discrete-Time Dynamical Systems

Problem Definition

The paper addresses the challenge of verifying discrete-time dynamical systems against $\omega$-regular properties, specifically those requiring the proof that a specific set of states (or a region) is visited only finitely often. Traditional safety verification ensures a system never enters an unsafe set. However, many temporal logic properties (e.g., those specified by Universal Co-Büchi Automata or the complement of Büchi automata) require demonstrating that a system does not visit an accepting state infinitely often.

Existing approaches face significant limitations:

1. State Triplet Approach: Previous methods (e.g., Wongpiromsarn et al.) use barrier certificates to "cut" paths in an automaton by breaking state triplets. While effective for finite-word automata or co-safe languages, this approach is conservative and often fails for general infinite-word automata. It cannot verify systems where traces reach an accepting state more than twice, even if the total visits are finite.
2. Bounded Synthesis Limitations: While bounded synthesis converts LTL specifications into safety problems by bounding state visitations, standard techniques often require unfolding the automaton or dealing with complex product constructions that lack incremental guarantees.
3. Complexity: Traditional model checking on continuous spaces suffers from the curse of dimensionality, while existing barrier certificate methods for temporal logic often rely on specific templates or lack necessity guarantees.

The core problem is to develop a functional overapproximation (a certificate) that proves a system's traces visit a specific region a bounded number of times, without explicitly constructing the full product system or unfolding the automaton indefinitely.

Methodology

The authors propose Co-Büchi Barrier Certificates (CBBCs), a generalization of classic barrier certificates. The methodology relies on the following conceptual and computational steps:

1. Conceptual Framework: Bounded Visitation as Safety

The core insight is that while "visiting a region finitely often" is not a direct safety property, it can be transformed into one by augmenting the system with a counter.

• Extended System: The original system $S$ is conceptually extended to $S'$ by appending a counter $\ell$ that increments every time the system enters the target region $X_{VF}$.
• Safety Reduction: Proving that $X_{VF}$ is visited finitely often is equivalent to proving that the extended system $S'$ never reaches a state where the counter exceeds a fixed bound $k$. This transforms the problem into a standard safety verification problem on the extended state space.

2. Definition of CBBCs

A Co-Büchi Barrier Certificate is a function $B: X \times [0..k] \to \mathbb{R}$ that satisfies specific conditions ensuring the counter never exceeds $k$:

• Initial Condition: $B(x, 0) \le 0$ for all initial states.
• Unsafe Condition: $B(x, k) > 0$ for all states in the target region $X_{VF}$ (indicating that reaching the region with a counter of $k$ is "unsafe").
• Inductive Step:
  • If the system is not in $X_{VF}$, the value of $B$ must be non-increasing (counter stays same).
  • If the system is in $X_{VF}$, the value of $B$ at the next step (with counter incremented) must be non-increasing relative to the current step.

The paper proves that the existence of such a function is both sufficient and necessary (under oracle assumptions) for the system to visit the region at most $k$ times.

3. Automata-Theoretic Verification

To verify properties specified by a Universal Co-Büchi Automaton (UCA) $A_{c,k}$:

• The system $S$ is synchronized with the automaton to form a product system.
• The "unsafe" region for the CBBC is defined as the set of product states where the automaton is in an accepting state.
• The verification algorithm searches for a CBBC with a bound $k$. If found, the system satisfies the property. If not, $k$ is incremented, and the search repeats. This provides an incremental verification approach.

4. Computational Approaches

The paper presents two methods to compute CBBCs:

1. Sum-of-Squares (SOS) Approach: Assumes the system dynamics and state sets are semi-algebraic (defined by polynomial inequalities). The search for the barrier certificate is cast as a semidefinite programming (SDP) problem. The complexity is polynomial in the dimension of the state space (assuming a fixed polynomial degree template) and linear in the bound $k$.
2. SMT-Based Approach (CEGIS): Uses Counterexample-Guided Inductive Synthesis. It samples points from the state space, encodes the CBBC constraints as Satisfiability Modulo Theories (SMT) queries over linear real arithmetic, and iteratively refines the candidate certificate using counterexamples until a valid function is found or a timeout occurs.

Key Contributions

1. Novel Certificate Definition: The introduction of Co-Büchi Barrier Certificates (CBBCs), which generalize classic barrier certificates to handle "finite visitation" properties by incorporating a counter variable directly into the certificate function.
2. Theoretical Guarantees: The paper establishes that CBBCs are not only sufficient but also necessary conditions for verifying bounded visitation properties, a stronger claim than many existing temporal verification methods.
3. Generalization of State Triplet Approach: The authors demonstrate that the CBBC approach subsumes the "state triplet" approach. They provide a constructive proof showing that if a system can be verified via the state triplet method, it can also be verified via CBBCs, but the converse is not true (CBBCs can verify systems the triplet method cannot).
4. Incremental Verification Strategy: The proposed methodology allows for an incremental search for the bound $k$. The algorithm starts with $k=0$ and increases the bound only when a certificate cannot be found, offering a practical trade-off between computational cost and verification power.
5. Computational Frameworks: The provision of both SOS-based (for polynomial systems) and SMT-based (for general systems) algorithms to synthesize these certificates.

Results and Case Studies

The paper validates the approach through three case studies:

1. Room Temperature Model (Failure of State Triplet): A system where the state triplet approach fails due to overlapping labels on automaton edges (specifically, the inability to cut paths with repeated labels). The CBBC approach successfully found a certificate with $k=4$, proving the property holds where the previous method was inconclusive.
2. 2D Van der Pol Oscillator: A nonlinear system verified against a UCA. Using the SOS approach, a degree-6 CBBC was found with $k=3$ in approximately 5 minutes, proving the accepting states are visited at most 3 times.
3. 3D Kuramoto Oscillator: A higher-dimensional system with trigonometric dynamics (approximated via Taylor series). A degree-4 CBBC was found with $k=2$ in approximately 20 minutes, verifying the finite visitation of a specific region.

Significance and Claims

The paper claims that CBBCs provide a robust, abstraction-free framework for verifying $\omega$-regular properties on discrete-time dynamical systems. Its significance lies in:

• Overcoming Conservatism: It addresses the limitations of the state triplet approach, which is often too conservative for general infinite-word automata.
• Scalability: By avoiding the explicit construction of complex product automata with large state spaces and relying on functional overapproximations, the method scales polynomially with the state dimension (for fixed templates), mitigating the curse of dimensionality.
• Necessity: Unlike many heuristic approaches, the paper argues for the necessity of these certificates, suggesting that if a system satisfies the property, a CBBC theoretically exists.

The authors note that while CBBCs are effective for verification, their application to synthesis (controller design) remains challenging due to the difficulties of handling nondeterminism and the need for deterministic automata in realizability problems. They identify this as a direction for future work, alongside extending the approach to weighted, stochastic, and timed automata.