Safety Barrier Certificates for Stochastic Hybrid Systems

TL;DR

This paper introduces a control barrier certificate framework for ensuring safety in stochastic hybrid systems with continuous stochastic dynamics and jumps, providing probabilistic safety guarantees without discretization.

Contribution

It develops an augmented control barrier certificate approach for stochastic hybrid systems, enabling safety synthesis and probabilistic guarantees in finite time horizons.

Findings

Framework successfully applied to a nonlinear case study.

Provides upper bounds on unsafe region reachability probabilities.

Offers a discretization-free safety verification method.

Abstract

This work is concerned with the safety controller synthesis of stochastic hybrid systems, in which continuous evolutions are described by stochastic differential equations with both Brownian motions and Poisson processes, and instantaneous jumps are governed by stochastic difference equations with additive noises. Our proposed framework leverages the notion of control barrier certificates (CBC), as a discretization-free approach, to synthesize safety controllers for stochastic hybrid systems while providing safety guarantees in finite time horizons. In our proposed scheme, we first provide an augmented framework to characterize each stochastic hybrid system containing continuous evolutions and instantaneous jumps with a unified system covering both scenarios. We then introduce an augmented control barrier certificate (ACBC) for augmented systems and propose sufficient conditions to construct an ACBC based on CBC of original hybrid systems. By utilizing the constructed ACBC, we quantify upper bounds on the probability that the stochastic hybrid system reaches certain unsafe regions in a finite time horizon. The proposed approach is verified over a nonlinear case study.