# Closure Certificates

arXiv: https://arxiv.org/abs/2305.17519 · HTML: https://mlsanity.com/paper/2305.17519/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 27 May 2023.

## Built on by (most cited first, 2 of 2)

- [Neural Model Checking](https://mlsanity.com/paper/2410.23790/) (2024)
- [Bisimulation Learning](https://mlsanity.com/paper/2405.15723/) (2024)

## Abstract (arXiv)

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.