Leveraging autonomous systems in safety-critical scenarios requires verifying their behaviors in the presence of uncertainties and black-box components that influence the system dynamics. In this work, we develop a framework for verifying discrete-time dynamical systems with unmodelled dynamics and noisy measurements against temporal logic specifications from an input-output dataset. The verification framework employs Gaussian process (GP) regression to learn the unknown dynamics from the dataset and abstracts the continuous-space system as a finite-state, uncertain Markov decision process (MDP). This abstraction relies on space discretization and transition probability intervals that capture the uncertainty due to the error in GP regression by using reproducible kernel Hilbert space analysis as well as the uncertainty induced by discretization. The framework utilizes existing model checking tools for verification of the uncertain MDP abstraction against a given temporal logic specification. We establish the correctness of extending the verification results on the abstraction created from noisy measurements to the underlying system. We show that the computational complexity of the framework is polynomial in the size of the dataset and discrete abstraction. The complexity analysis illustrates a trade-off between the quality of the verification results and the computational burden to handle larger datasets and finer abstractions. Finally, we demonstrate the efficacy of our learning and verification framework on several case studies with linear, nonlinear, and switched dynamical systems.

翻译：在安全关键场景中部署自主系统时，需在存在不确定性和影响系统动态的黑盒组件条件下验证其行为。本研究针对具有未建模动态特性与噪声测量的离散时间动态系统，提出一种基于输入-输出数据集验证其时序逻辑规约的框架。该验证框架采用高斯过程回归从数据集中学习未知动态特性，并将连续空间系统抽象为有限状态不确定马尔可夫决策过程。该抽象方法依赖于空间离散化及转移概率区间，通过再生核希尔伯特空间分析捕获高斯过程回归误差引起的不确定性，同时涵盖离散化引入的不确定性。框架利用现有模型检验工具对不确定MDP抽象进行给定时序逻辑规约的验证。我们证明了将基于噪声测量构建的抽象模型验证结果扩展至底层系统的正确性。研究表明该框架的计算复杂度在数据集规模和离散抽象维度上呈多项式增长。复杂度分析揭示了验证结果质量与处理更大数据集及更精细抽象的计算负担之间的权衡关系。最后，我们通过线性、非线性和切换动态系统的多个案例研究验证了所提学习与验证框架的有效性。