Almost Sure Reachability in Continuous-time Stochastic Systems

TL;DR

This paper develops continuous-time certificates for almost sure reachability in stochastic systems, overcoming discretization issues and enabling verification via sum-of-squares methods.

Contribution

It introduces new certificates for continuous-time stochastic systems and demonstrates their effectiveness, especially for polynomial SDEs, using SOS techniques.

Findings

Discretization may fail to preserve reachability properties.

Certificates accurately verify almost sure reachability in continuous systems.

SOS methods successfully verify reachability in polynomial SDEs.

Abstract

We provide certificates for almost sure reachability of continuous-time stochastic systems governed by stochastic differential equations (SDEs). We first show that a standard Euler-Maruyama discretization may fail to preserve almost sure reachability property of the system using a double-well Langevin system. This observation motivates us to develop certificates for almost sure reachability directly on the continuous-time system. We introduce a pair of certificates, a drift function and a variant function, and prove necessity and sufficiency for almost sure reachability of an open bounded target set. Using these certificates, for linear SDEs, we give a characterization of almost sure reachability in terms of the spectral structure of the system matrices. For polynomial SDEs, we fix a polynomial template for the drift function and choose the variant function template as an exponential function composed with a polynomial. This allows us to translate the conditions in the certificates into sum-of-squares (SOS) constraints. We then propose an alternating scheme to resolve bilinearities. We illustrate the approach on the double-well Langevin example, showing that continuous-time SOS certificates recover almost sure reachability that is lost under time discretization. Moreover, we verify the SOS approach on a polynomial system.