Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Closure Certificates

Vishnu Murali, Ashutosh Trivedi, Majid Zamani

TL;DR

The paper addresses automated verification of omega-regular specifications for discrete-time dynamical systems by introducing closure certificates, a functional generalization of barrier certificates that captures transitive transition invariants. It presents two practical synthesis routes—SMT-based counterexample-guided synthesis and SOS-based polynomial certificates—to find closure certificates over SSP templates, enabling verification of safety, persistence, and LTL properties via product with NBA automata. The approach subsumes existing state-triplet barrier methods and demonstrates its effectiveness through Kuramoto oscillator and two-room temperature case studies, yielding certificates and quantitative performance data. This abstraction-free framework expands the repertoire of verifiable properties for cyber-physical systems and suggests avenues for data-driven CC discovery and controller synthesis with broad practical impact.

Abstract

A barrier certificate, defined over the states of a dynamical system, is a real-valued function whose zero level set characterizes an inductively verifiable state invariant separating reachable states from unsafe ones. When combined with powerful decision procedures such as sum-of-squares programming (SOS) or satisfiability-modulo-theory solvers (SMT) barrier certificates enable an automated deductive verification approach to safety. The barrier certificate approach has been extended to refute omega-regular specifications by separating consecutive transitions of omega-automata in the hope of denying all accepting runs. Unsurprisingly, such tactics are bound to be conservative as refutation of recurrence properties requires reasoning about the well-foundedness of the transitive closure of the transition relation. This paper introduces the notion of closure certificates as a natural extension of barrier certificates from state invariants to transition invariants. We provide SOS and SMT based characterization for automating the search of closure certificates and demonstrate their effectiveness via a paradigmatic case study.

Closure Certificates

TL;DR

The paper addresses automated verification of omega-regular specifications for discrete-time dynamical systems by introducing closure certificates, a functional generalization of barrier certificates that captures transitive transition invariants. It presents two practical synthesis routes—SMT-based counterexample-guided synthesis and SOS-based polynomial certificates—to find closure certificates over SSP templates, enabling verification of safety, persistence, and LTL properties via product with NBA automata. The approach subsumes existing state-triplet barrier methods and demonstrates its effectiveness through Kuramoto oscillator and two-room temperature case studies, yielding certificates and quantitative performance data. This abstraction-free framework expands the repertoire of verifiable properties for cyber-physical systems and suggests avenues for data-driven CC discovery and controller synthesis with broad practical impact.

Abstract

A barrier certificate, defined over the states of a dynamical system, is a real-valued function whose zero level set characterizes an inductively verifiable state invariant separating reachable states from unsafe ones. When combined with powerful decision procedures such as sum-of-squares programming (SOS) or satisfiability-modulo-theory solvers (SMT) barrier certificates enable an automated deductive verification approach to safety. The barrier certificate approach has been extended to refute omega-regular specifications by separating consecutive transitions of omega-automata in the hope of denying all accepting runs. Unsurprisingly, such tactics are bound to be conservative as refutation of recurrence properties requires reasoning about the well-foundedness of the transitive closure of the transition relation. This paper introduces the notion of closure certificates as a natural extension of barrier certificates from state invariants to transition invariants. We provide SOS and SMT based characterization for automating the search of closure certificates and demonstrate their effectiveness via a paradigmatic case study.
Paper Structure (25 sections, 11 theorems, 23 equations, 6 figures)

This paper contains 25 sections, 11 theorems, 23 equations, 6 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Discrete-time Dynamical System
  4. Specifications
  5. Closure Certificates
  6. Closure Certificates for Safety
  7. Closure Certificates for Persistence
  8. Closure Certificates for LTL Specifications
  9. Synthesizing Closure Certificates
  10. SMT-based Approach
  11. Sum-of-Squares based Approach
  12. Subsuming Existing Approaches
  13. The State Triplet Approach
  14. CC Subsumes State Triplet Approach
  15. Case Studies
  16. ...and 10 more sections

Key Result

Theorem 1

For a system $\mathfrak{S}$ with unsafe states $\mathcal{X}_u$, the existence of a barrier certificate $\mathcal{B}$ implies its safety.

Figures (6)

  • Figure 1: Illustrative example demonstrating the simplicity of closure certificates over barrier certificates
  • Figure 2: Example NBA $\mathcal{A}$ which represents the complement of a safety to illustrate the state triplet approach.
  • Figure 3: Example NBA $\mathcal{A}$ (Figure \ref{['subfig:aut_unroll']}) and its unrolling (Figure \ref{['subfig:aut_unrolled']}) from Section \ref{['subsec:triplet']}.
  • Figure 4: A (nondeterministic) Büchi automaton $\mathcal{A}$ representing the LTL formula $\mathsf{F} a$.
  • Figure 5: A (nondeterministic) Büchi automaton $\mathcal{A}$ for the two-room temperature case study from Section \ref{['sec:case_studies']}. The automata represents the LTL formula $a_0 \wedge \mathsf{G} \mathsf{F} a_1$. Here $\top$ indicates any letter in the alphabet.
  • ...and 1 more figures

Theorems & Definitions (15)

  • Definition 2.1: Barrier Certificate
  • Theorem 1: Barrier certificates imply safety prajna_2004_safety
  • Definition 3.1: Closure Certificate for Safety
  • Theorem 2: Closure Certificate imply Safety
  • Theorem 3: Simplicity of Closure Certificates
  • Theorem 4: Expressiveness
  • Definition 3.2: Closure Certificates for Persistence
  • Theorem 5: Closure Certificates imply Persistence
  • Definition 3.3: Closure Certificate for LTL
  • Theorem 6: Closure Certificates verify LTL
  • ...and 5 more