On Certificates for Almost Sure Reachability in Stochastic Systems

TL;DR

This paper investigates the certification of almost sure reachability in stochastic systems, revealing limitations of fixed-template methods and providing a complete characterization for linear systems with additive noise.

Contribution

It demonstrates the incompleteness of polynomial and quadratic templates and offers a full characterization of reachability certificates for linear stochastic systems.

Findings

Polynomial systems may lack polynomial certificates despite being almost surely reachable.

Linear systems can be almost surely reachable without quadratic certificates.

Conditions are provided for the existence of certificates based on system matrices.

Abstract

Almost sure reachability refers to the property of a stochastic system whereby, from any initial condition, the system state reaches a given target set with probability one. In this paper, we study the problem of certifying almost sure reachability in discrete-time stochastic systems using drift and variant conditions. While these conditions are both necessary and sufficient in theory, computational approaches often rely on restricting the search to fixed templates, such as polynomial or quadratic functions. We show that this restriction compromises completeness: there exists a polynomial system for which a given target set is almost surely reachable but admits no polynomial certificate, and a linear system for which a neighborhood of the origin is almost surely reachable but admits no quadratic certificate. We then provide a complete characterization of reachability certificates for linear systems with additive noise. Our analysis yields conditions on the system matrices under which valid certificates exist, and shows how the structure and dimension of the system determine the need for non-quadratic templates. Our results generalize the classical random walk behavior to a broader class of stochastic dynamical systems.