Almost Sure Reachability in Continuous-time Stochastic Systems
For researchers in stochastic control and verification, this work addresses a fundamental gap by providing direct continuous-time certificates for almost sure reachability, which is incremental over existing discrete-time methods.
The paper provides certificates for almost sure reachability in continuous-time stochastic systems, showing that Euler-Maruyama discretization can fail to preserve this property. The approach uses drift and variant functions, with sum-of-squares constraints for polynomial systems, and is demonstrated on examples including a double-well Langevin system.
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.