Myopically Verifiable Probabilistic Certificate for Long-term Safety

TL;DR

This paper introduces a novel probabilistic safety certificate for stochastic systems that guarantees long-term safety by framing safety as a forward invariance on probability space, enabling efficient evaluation and control.

Contribution

It proposes a new notion of forward invariance on probability space for long-term safety, and develops a controller that guarantees safe probability without extensive horizon computation.

Findings

The controller guarantees non-decreasing safe probability over time.

Numerical simulations validate the effectiveness of the proposed safety framework.

Framework can be adapted for finite-time Lyapunov analysis in stochastic systems.

Abstract

In this paper, we consider the use of barrier function-based approaches for the safe control problem in stochastic systems. With the presence of stochastic uncertainties, a myopic controller that ensures safe probability in infinitesimal time intervals may allow the accumulation of unsafe probability over time and result in a small long-term safe probability. Meanwhile, increasing the outlook time horizon may lead to significant computation burdens and delayed reactions, which also compromises safety. To tackle this challenge, we define a new notion of forward invariance on probability space as opposed to the safe regions on state space. This new notion allows the long-term safe probability to be framed into a forward invariance condition, which can be efficiently evaluated. We build upon this safety condition to propose a controller that works myopically yet can guarantee long-term safe probability or fast recovery probability. The proposed controller ensures the safe probability does not decrease over time and allows the designers to directly specify safe probability. The performance of the proposed controller is then evaluated in numerical simulations. Finally, we show that this framework can also be adapted to characterize the speed and probability of forward convergent behaviors, which can be of use to finite-time Lyapunov analysis in stochastic systems.