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. 渐进稳定性，并首次提供了获得稳定时间上界的方法，这是随机李雅普诺夫函数所没有的。

神经网络超马丁格尔稳定性检验在随机控制系统中的应用

Stability Verification in Stochastic Control Systems via Neural Network  Supermartingales

In this paper, we consider termination of probabilistic programs with
real-valued variables. The questions concerned are:
1. qualitative ones that ask (i) whether the program terminates with
probability 1 (almost-sure termination) and (ii) whether the expected
termination time is finite (finite termination); 2. quantitative ones that ask
(i) to approximate the expected termination time (expectation problem) and (ii)
to compute a bound B such that the probability to terminate after B steps
decreases exponentially (concentration problem).
To solve these questions, we utilize the notion of ranking supermartingales
which is a powerful approach for proving termination of probabilistic programs.
In detail, we focus on algorithmic synthesis of linear ranking-supermartingales
over affine probabilistic programs (APP's) with both angelic and demonic
non-determinism. An important subclass of APP's is LRAPP which is defined as
the class of all APP's over which a linear ranking-supermartingale exists.
Our main contributions are as follows. Firstly, we show that the membership
problem of LRAPP (i) can be decided in polynomial time for APP's with at most
demonic non-determinism, and (ii) is NP-hard and in PSPACE for APP's with
angelic non-determinism; moreover, the NP-hardness result holds already for
APP's without probability and demonic non-determinism. Secondly, we show that
the concentration problem over LRAPP can be solved in the same complexity as
for the membership problem of LRAPP. Finally, we show that the expectation
problem over LRAPP can be solved in 2EXPTIME and is PSPACE-hard even for APP's
without probability and non-determinism (i.e., deterministic programs). Our
experimental results demonstrate the effectiveness of our approach to answer
the qualitative and quantitative questions over APP's with at most demonic
non-determinism.

本文研究带有实值变量的概率程序的终止性问题，并利用排名超级鞅的概念解决了定性和定量问题，特别是在关于 LRAPP 的多个方面做出了贡献。