Formal Verification of Unknown Dynamical Systems via Gaussian Process Regression

TL;DR

This work addresses certifiable verification of unknown discrete-time dynamical systems with measurement noise by learning the latent dynamics via Gaussian process regression and quantifying the learning error through RKHS-based bounds. The authors build a sound finite-state abstraction in the form of an Interval Markov Decision Process (IMDP) that captures both learning and discretization uncertainties, and then verify the abstraction against PCTL specifications using standard model-checking tools. A key contribution is a correctness result showing that verification results on the IMDP extend to guarantees about the latent system, accompanied by a detailed complexity analysis highlighting a polynomial dependence on dataset size $d$ and the discretization. The framework is demonstrated across linear, nonlinear, and switched systems, including a 3D Dubin's car, illustrating practical data-driven certification for safety-critical applications and outlining pathways to scale with larger datasets and finer abstractions.

Abstract

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.

Figures (8)

• Figure 1: Overview of our learning-based, formal verification framework.
• Figure 2: The unbounded ($k=\infty$) verification results for the known system and learned system using increasingly large datasets subject to $\phi=\textnormal{P}_{\geq0.95}[\neg O~\mathcal{U}~D$].
• Figure 3: Verification using our approach (colors) and SOS barriers (outlines) for the known and learned systems. Bold outlines indicate a satisfying barrier is found for that state, while dashed Xs indicate the barrier does not satisfy safety.
• Figure 4: Effect of the size of discretization and $\epsilon$ on the average satisfaction probability interval size (verification error).
• Figure 5: Verification results for the switched system subject to $\phi=\textnormal{P}_{\geq0.95} [\mathcal{G}^{\leq k} X]$.

Theorems & Definitions (22)

• Definition 1: PCTL Syntax
• Definition 2: PCTL Semantics
• Remark 1
• Proposition 1: chowdhury2017kernelized, Theorem 2
• Definition 3: Interval MDP
• Definition 4: Strategy
• Definition 5: Adversary
• Proposition 2: RKHS Norm Bound
• Remark 2
• Proposition 3: Information Gain Bound