# Barrier Certificates Revisited

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

## Key facts

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

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

- [System-level Safety Guard: Safe Tracking Control through Uncertain Neural Network Dynamics Models](https://mlsanity.com/paper/2312.06810/) (2023)
- [Set-Based Training of Neural Barrier Certificates for Safety Verification of Dynamical Systems](https://mlsanity.com/paper/2605.02526/) (2026)

## Abstract (arXiv)

A barrier certificate can separate the state space of a con- sidered hybrid system (HS) into safe and unsafe parts ac- cording to the safety property to be verified. Therefore this notion has been widely used in the verification of HSs. A stronger condition on barrier certificates means that less expressive barrier certificates can be synthesized. On the other hand, synthesizing more expressive barrier certificates often means high complexity. In [9], Kong et al consid- ered how to relax the condition of barrier certificates while still keeping their convexity so that one can synthesize more expressive barrier certificates efficiently using semi-definite programming (SDP). In this paper, we first discuss how to relax the condition of barrier certificates in a general way, while still keeping their convexity. Particularly, one can then utilize different weaker conditions flexibly to synthesize dif- ferent kinds of barrier certificates with more expressiveness efficiently using SDP. These barriers give more opportuni- ties to verify the considered system. We also show how to combine two functions together to form a combined barrier certificate in order to prove a safety property under consid- eration, whereas neither of them can be used as a barrier certificate separately, even according to any relaxed condi- tion. Another contribution of this paper is that we discuss how to discover certificates from the general relaxed condi- tion by SDP. In particular, we focus on how to avoid the unsoundness because of numeric error caused by SDP with symbolic checking
