Sum-of-Squares Certificates for Almost-Sure Reachability of Stochastic Polynomial Systems

TL;DR

This work addresses certifying almost-sure reachability for discrete-time polynomial stochastic systems by transforming drift–variant conditions into sum-of-squares programs solvable as semidefinite programs. It introduces a dual SOS framework: (i) a drift certificate $V$ that is radially unbounded and nonincreasing in expectation outside a compact set, and (ii) a variant certificate $U$ that achieves a one-step decrease with positive probability on a disturbance ball, enforced via the S-procedure with polynomial multipliers. An alternating optimization scheme resolves bilinear couplings between $V$, $U$, multipliers, and the disturbance radius, yielding practical, solver-ready certificates with quantitative margins. Two nonlinear examples demonstrate the workflow: one with additive disturbance and one with multiplicative disturbance, illustrating how the approach certifies almost-sure reachability and provides interpretable SOS-based certificates that can guide verification and potential controller synthesis in stochastic settings.

Abstract

In this paper, we present a computational approach to certify almost sure reachability for discrete-time polynomial stochastic systems by turning drift--variant criteria into sum-of-squares (SOS) programs solved with standard semidefinite solvers. Specifically, we provide an SOS method based on two complementary certificates: (i) a drift certificate that enforces a radially unbounded function to be non-increasing in expectation outside a compact set of states; and (ii) a variant certificate that guarantees a one-step decrease with positive probability and ensures the target contains its nonpositive sublevel set. We transform these conditions to SOS constraints. For the variant condition, we enforce a robust decrease over a parameterized disturbance ball with nonzero probability and encode the constraints via an S-procedure with polynomial multipliers. The resulting bilinearities are handled by an alternating scheme that alternates between optimizing multipliers and updating the variant and radius until a positive slack is obtained. Two case studies illustrate the workflow and certifies almost-sure reachability.

Figures (8)

• Figure 1: Stochastic trajectories of the system from various initial states.
• Figure 2: SOS-based drift certification. Left: The certified drift function $V(x)$. This shows that $V(x)$ grows radially, satisfying the unboundedness condition. Right: The drift decrement $\Delta V(x) = \mathbb{E}[V(f(x, w))] - V(x)$. The black contour marks the zero level set and outside of the contour is for $\Delta V(x)\leq 0$.
• Figure 3: SOS-based variant certification. Left: Surface of $U(x)$ with the contour $U(x)=0$ (black) and the target-set boundary $\partial G$ (red), showing $\{x:\,U(x)\le 0\}\subseteq G$. Right:$\min_{\|w\|^2\le \rho^\star}\![\,U(x)-U(f(x,w))-\delta\,]$ over the state space. For all states with $U(x)>0$, the quantity $U(x)-U(f(x,w))-\delta$ is nonnegative for every disturbance $\|w\|^2\le \rho^\star$, certifying a uniform one-step decrease on a non-empty set.
• Figure 4: Evolution of $\rho_k$ (top) and the slack $\varepsilon_k$ (bottom) across iterations of Algorithm \ref{['alg:variant-sos']}.
• Figure 5: Stochastic trajectories of the multiplicative-noise system from various initial conditions. Each color corresponds to a distinct starting point on a circle of radius $10$.

Theorems & Definitions (5)

• Definition 1
• Theorem 1: Almost sure reachability
• Example 1
• Remark 1
• Remark 2