On the Construction of Barrier Certificate: A Dynamic Programming Perspective

TL;DR

This paper introduces a new, less conservative method for constructing barrier certificates in stochastic dynamical systems, improving safety probability bounds through a dynamic programming perspective and SOS programming.

Contribution

It offers a novel dynamic programming interpretation of barrier certificates, resulting in tighter safety bounds and extending the approach to reach-avoid specifications.

Findings

New barrier conditions are less conservative than existing ones.

The approach provides tighter safety probability bounds.

Numerical examples demonstrate improved performance.

Abstract

In this paper, we revisit the formal verification problem for stochastic dynamical systems over finite horizon using barrier certificates. Most existing work on this topic focuses on safety properties by constructing barrier certificates based on the notion of $c$-martingales. In this work, we first provide a new insight into the conditions of existing martingale-based barrier certificates from the perspective of dynamic programming operators. Specifically, we show that the existing conditions essentially provide a bound on the dynamic programming solution, which exactly characterizes the safety probability. Based on this new perspective, we demonstrate that the barrier conditions in existing approaches are unnecessarily conservative over unsafe states. To address this, we propose a new set of safety barrier certificate conditions that are strictly less conservative than existing ones, thereby providing tighter probability bounds for safety verification. We further extend our approach to the case of reach-avoid specifications by providing a set of new barrier certificate conditions. We also illustrate how to search for these new barrier certificates using sum-of-squares (SOS) programming. Finally, we use two numerical examples to demonstrate the advantages of our method compared to existing approaches.