标题： 通过非参数估计对未知随机系统进行形式化验证 显示英文标题

标题： Formal Verification of Unknown Stochastic Systems via Non-parametric Estimation

摘要： 一种新的数据驱动方法用于形式化验证，以研究在安全关键领域运行的复杂系统。 所提出的方法仅使用观察样本，而无需了解模型，就能够对离散时间随机动力系统进行形式化验证，并提供关于规范满足的概率保证。 我们首先提出了理论结果，用于使用非参数估计来估计随机系统的\emph{Lipschitz常数}的渐近上界，这可以确定系统的有限抽象。 我们的结果证明了估计的渐近收敛速率为$O(n^{-\frac{1}{3+d}})$，其中$d$是系统的维度，$n$是数据规模。 然后，我们使用两种不同的数据驱动方法，即转移概率的非参数估计和经验估计，构建区间马尔可夫决策过程，以针对给定的时间逻辑规范进行形式化验证。 多个案例研究被提出以验证所提出方法的有效性。 显示英文摘要

摘要： A novel data-driven method for formal verification is proposed to study complex systems operating in safety-critical domains. The proposed approach is able to formally verify discrete-time stochastic dynamical systems against temporal logic specifications only using observation samples and without the knowledge of the model, and provide a probabilistic guarantee on the satisfaction of the specification. We first propose the theoretical results for using non-parametric estimation to estimate an asymptotic upper bound for the \emph{Lipschitz constant} of the stochastic system, which can determine a finite abstraction of the system. Our results prove that the asymptotic convergence rate of the estimation is $O(n^{-\frac{1}{3+d}})$, where $d$ is the dimension of the system and $n$ is the data scale. We then construct interval Markov decision processes using two different data-driven methods, namely non-parametric estimation and empirical estimation of transition probabilities, to perform formal verification against a given temporal logic specification. Multiple case studies are presented to validate the effectiveness of the proposed methods.