发表机构
University of Southampton; MPI-SWS; University of Birmingham（南安普顿大学; 马克斯·普朗克软件系统研究所; 伯明翰大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出一种基于非参数估计的数据驱动方法，仅利用观测样本即可对未知随机系统进行形式验证与策略综合，并证明转移概率和利普希茨常数的估计具有渐近收敛保证。
AI 中文摘要
数据驱动技术在检查运行于安全关键领域的复杂系统是否满足安全性及其他时序要求方面已展现出巨大潜力。本文研究一类基于非参数估计、从数据中学习系统表示的数据驱动技术。所提出的方法仅利用观测样本，在无需模型知识的情况下，能够针对时序逻辑规范对离散时间随机动力系统进行形式验证，并为规范的满足提供概率性保证。我们首先考虑以马尔可夫决策过程（MDPs）形式表示系统的有限抽象，并利用伯恩斯坦不等式和非参数估计器的统计性质，推导出抽象MDP的转移概率与其估计值之间的渐近收敛保证。随后，我们提出用于估计随机系统利普希茨常数（LC）渐近上界的理论结果，该上界可在给定精度误差下确定有限抽象MDP的规模。在适当假设下，我们的结果证明，对于转移概率和LC，估计的渐近收敛速率均为$O(n^{-1/(3+d)})$，其中$\mathsf d$为系统维度，$n$为数据规模。通过整合这些结果，我们能够保证基于数据集规模对原始系统及其有限抽象所执行的形式验证和策略综合的渐近接近性。文中还呈现了多个案例研究，以验证所提出方法的有效性。
英文摘要
Data-driven techniques have shown promising potential for checking behavior of complex systems operating in safety-critical domains against safety and other temporal requirements. This paper studies a class of data-driven techniques that are based on learning a representation of the system from data using non-parametric estimation. 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 provides a probabilistic guarantee on the satisfaction of the specification. We first consider finite abstract representations of the system in the form of Markov decision processes (MDPs) and derive asymptotic convergence guarantees between the transition probabilities of the abstract MDP and their estimation using Bernstein's inequality and statistical properties of non-parametric estimators. We then propose theoretical results for estimating the asymptotic upper bound of the \emph{Lipschitz constant} (LC) of the stochastic system, which can determine the size of the finite abstract MDP for a given precision error. Under appropriate assumptions, our results prove that the asymptotic convergence rate of the estimations is $O(n^{-1/(3+d)})$ for both the transition probabilities and the LC, where $\mathsf d$ is the dimension of the system and $n$ is the data scale. By integrating these results, we can guarantee the asymptotic closeness in formal verification and policy synthesis performed on the original system and its finite abstraction based on the size of the dataset. Multiple case studies are presented to validate the effectiveness of the proposed method.
