We consider the problem of formally verifying almost-sure (a.s.) asymptotic
stability in discrete-time nonlinear stochastic control systems. While
verifying stability in deterministic control systems is extensively studied in
the literature, verifying stability in stochastic control systems is an open
problem. The few existing works on this topic either consider only specialized
forms of stochasticity or make restrictive assumptions on the system, rendering
them inapplicable to learning algorithms with neural network policies. In this
work, we present an approach for general nonlinear stochastic control problems
with two novel aspects: (a) instead of classical stochastic extensions of
Lyapunov functions, we use ranking supermartingales (RSMs) to certify
a.s.~asymptotic stability, and (b) we present a method for learning neural
network RSMs. We prove that our approach guarantees a.s.~asymptotic stability
of the system and provides the first method to obtain bounds on the
stabilization time, which stochastic Lyapunov functions do not. Finally, we
validate our approach experimentally on a set of nonlinear stochastic
reinforcement learning environments with neural network policies.

我们提出了一种使用 Ranking Supermartingales（RSMs）证明绝大多数（a.s.）渐进稳定性的方法，同时还提出了一种学习神经网络 RSMs 的方法。我们的方法保证系统的 a.s. 渐进稳定性，并首次提供了获得稳定时间上界的方法，这是随机李雅普诺夫函数所没有的。