# Verification and Control for Finite-Time Safety of Stochastic Systems via Barrier Functions

## TL;DR

This paper introduces a novel approach using stochastic barrier functions and sum-of-squares optimization to verify and control the finite-time safety probabilities of stochastic systems, including controller synthesis for affine-in-control dynamics.

## Contribution

It proposes a new barrier certificate condition with a state-dependent bound and a method for synthesizing polynomial controllers to ensure safety probabilities.

## Key findings

- Efficient numerical computation via sum-of-squares optimization.
- Tighter probability bounds through state-dependent infinitesimal generator bounds.
- Controller synthesis achieving specified safety probabilities.

## Abstract

This paper studies the problem of enforcing safety of a stochastic dynamical system over a finite time horizon. We use stochastic barrier functions as a means to quantify the probability that a system exits a given safe region of the state space in finite time. A barrier certificate condition that bounds the infinitesimal generator of the system, and hence bounds the expected value of the barrier function over the time horizon, is recast as a sum-of-squares optimization problem for efficient numerical computation. Unlike prior works, the proposed certificate condition includes a state-dependent bound on the infinitesimal generator, allowing for tighter probability bounds. Moreover, for stochastic systems for which the drift dynamics are affine-in-control, we propose a method for synthesizing polynomial state feedback controllers that achieve a specified probability of safety. Two case studies are presented that benchmark and illustrate the performance of our method.