Stochastic Barrier Certificates in the Presence of Dynamic Obstacles

TL;DR

This paper develops stochastic barrier certificates for dynamic obstacle environments, providing probabilistic safety guarantees for uncertain systems with improved accuracy and computational efficiency.

Contribution

It introduces time-varying barrier certificates formulated as convex sum-of-squares programs, enabling scalable safety verification in dynamic, uncertain environments.

Findings

Time-varying certificates offer less conservative safety bounds.

Convex sum-of-squares formulation enables tractable synthesis.

Empirical results show improved safety guarantees over existing methods.

Abstract

Safety of stochastic dynamic systems in environments with dynamic obstacles is studied in this paper through the lens of stochastic barrier functions. We introduce both time-invariant and time-varying barrier certificates for discrete-time, continuous-space systems subject to uncertainty, which provide certified lower bounds on the probability of remaining within a safe set over a finite horizon. These certificates explicitly account for time-varying unsafe regions induced by obstacle dynamics. By leveraging Bellman's optimality perspective, the time-varying formulation directly captures temporal structure and yields less conservative bounds than state-of-the-art approaches. By restricting certificates to polynomial functions, we show that time-varying barrier synthesis can be formulated as a convex sum-of-squares program, enabling tractable optimization. Empirical evaluations on nonlinear systems with dynamic obstacles show that time-varying certificates consistently achieve tight guarantees, demonstrating improved accuracy and scalability over state-of-the-art methods.