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 article, we develop a framework for
verifying partially-observable, discrete-time dynamical systems with unmodelled
dynamics against temporal logic specifications from a given input-output
dataset. The verification framework employs Gaussian process (GP) regression to
learn the unknown dynamics from the dataset and abstract 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 to the underlying partially-observable 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.

本文提出了一个基于高斯过程回归的验证框架，将连续空间系统抽象为有限状态不确定马尔可夫决策过程，利用模型检测工具验证抽象的不确定性，并将结果扩展到基础的部分可观测系统，有效地应用于线性、非线性和切换系统等多种情况下。