标题： 未知动力学系统的高斯过程回归形式验证 显示英文标题

标题： Formal Verification of Unknown Dynamical Systems via Gaussian Process Regression

摘要： 在安全关键场景中利用自主系统需要验证其行为是否能在存在不确定性和影响系统动力学的黑盒组件的情况下成立。在这项工作中，我们开发了一个框架，用于根据输入-输出数据集验证具有未建模动力学和噪声测量值的离散时间动态系统的时序逻辑规范。该验证框架使用高斯过程（GP）回归从数据集中学习未知的动力学，并将连续空间系统抽象为有限状态的不确定马尔可夫决策过程（MDP）。这种抽象依赖于空间离散化和捕获高斯过程回归误差以及由离散化引起的不确定性所带来的过渡概率区间。该框架利用现有的模型检测工具来验证不确定的MDP抽象是否符合给定的时序逻辑规范。我们证明了将基于噪声测量值创建的抽象上的验证结果扩展到底层系统的正确性。我们表明该框架的计算复杂度在数据集大小和离散抽象的规模上呈多项式增长。复杂度分析展示了验证结果质量和处理更大数据集和更精细抽象的计算负担之间的权衡。最后，我们在几个线性、非线性和切换动态系统的案例研究中展示了我们学习和验证框架的有效性。 显示英文摘要

摘要： 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.