# Formal Verification of Unknown Dynamical Systems via Gaussian Process Regression

arXiv: https://arxiv.org/abs/2201.00655 · HTML: https://mlsanity.com/paper/2201.00655/

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- Builds on 30 of its 80 references that are in the map.
- First posted on arXiv 31 Dec 2021.

## Builds on (most cited first, 30 of 30)

- [Aleatoric and Epistemic Uncertainty in Machine Learning: An Introduction to Concepts and Methods](https://mlsanity.com/paper/1910.09457/) (2019)
- [Safe Model-based Reinforcement Learning with Stability Guarantees](https://mlsanity.com/paper/1705.08551/) (2017)
- [On Kernelized Multi-armed Bandits](https://mlsanity.com/paper/1704.00445/) (2017)
- [On the Sample Complexity of the Linear Quadratic Regulator](https://mlsanity.com/paper/1710.01688/) (2017)
- [On Information Gain and Regret Bounds in Gaussian Process Bandits](https://mlsanity.com/paper/2009.06966/) (2020)
- [Uniform Error Bounds for Gaussian Process Regression with Application to Safe Control](https://mlsanity.com/paper/1906.01376/) (2019)
- [Safe Learning of Regions of Attraction for Uncertain, Nonlinear Systems with Gaussian Processes](https://mlsanity.com/paper/1603.04915/) (2016)
- [Planning with Learned Dynamics: Probabilistic Guarantees on Safety and Reachability via Lipschitz Constants](https://mlsanity.com/paper/2010.08993/) (2020)
- [Verification for Machine Learning, Autonomy, and Neural Networks Survey](https://mlsanity.com/paper/1810.01989/) (2018)
- [Formal Synthesis of Stochastic Systems via Control Barrier Certificates](https://mlsanity.com/paper/1905.04585/) (2019)
- [Control Barrier Functions for Unknown Nonlinear Systems using Gaussian Processes](https://mlsanity.com/paper/2010.05818/) (2020)
- [DRYVR:Data-driven verification and compositional reasoning for automotive systems](https://mlsanity.com/paper/1702.06902/) (2017)
- [Scalable Learning of Safety Guarantees for Autonomous Systems using Hamilton-Jacobi Reachability](https://mlsanity.com/paper/2101.05916/) (2021)
- [Data-Driven Reachability Analysis from Noisy Data](https://mlsanity.com/paper/2105.07229/) (2021)
- [Sampling-Based Robust Control of Autonomous Systems with Non-Gaussian Noise](https://mlsanity.com/paper/2110.12662/) (2021)
- [FAUST2: Formal Abstractions of Uncountable-STate STochastic processes](https://mlsanity.com/paper/1403.3286/) (2014)
- [Efficiency through Uncertainty: Scalable Formal Synthesis for Stochastic Hybrid Systems](https://mlsanity.com/paper/1901.01576/) (2019)
- [Adversarial Robustness Guarantees for Classification with Gaussian Processes](https://mlsanity.com/paper/1905.11876/) (2019)
- [Learning-based Symbolic Abstractions for Nonlinear Control Systems](https://mlsanity.com/paper/2004.01879/) (2020)
- [Provably Robust Learning-Based Approach for High-Accuracy Tracking Control of Lagrangian Systems](https://mlsanity.com/paper/1804.01031/) (2018)
- [Safety Verification of Unknown Dynamical Systems via Gaussian Process Regression](https://mlsanity.com/paper/2004.01821/) (2020)
- [PAC Model Checking of Black-Box Continuous-Time Dynamical Systems](https://mlsanity.com/paper/2007.10141/) (2020)
- [Data-driven computation of invariant sets of discrete time-invariant black-box systems](https://mlsanity.com/paper/1907.12075/) (2019)
- [Strategy Synthesis for Partially-known Switched Stochastic Systems](https://mlsanity.com/paper/2104.02172/) (2021)
- [Data Driven Stability Analysis of Black-box Switched Linear Systems](https://mlsanity.com/paper/1803.03687/) (2018)
- [Multi-objective Robust Strategy Synthesis for Interval Markov Decision Processes](https://mlsanity.com/paper/1706.06875/) (2017)
- [Safe Approximate Dynamic Programming Via Kernelized Lipschitz Estimation](https://mlsanity.com/paper/1907.02151/) (2019)
- [Simple, Fast and Practicable Algorithms for Cholesky, LU and QR Decomposition Using Fast Rectangular Matrix Multiplication](https://mlsanity.com/paper/1812.02056/) (2018)
- [Abstracting the Sampling Behaviour of Stochastic Linear Periodic Event-Triggered Control Systems](https://mlsanity.com/paper/2103.13839/) (2021)
- [Synergistic Offline-Online Control Synthesis via Local Gaussian Process Regression](https://mlsanity.com/paper/2110.05525/) (2021)

## Built on by (most cited first, 5 of 5)

- [Risk Verification of Stochastic Systems with Neural Network Controllers](https://mlsanity.com/paper/2209.09881/) (2022)
- [Promises of Deep Kernel Learning for Control Synthesis](https://mlsanity.com/paper/2309.06569/) (2023)
- [Data-Driven Permissible Safe Control with Barrier Certificates](https://mlsanity.com/paper/2405.00136/) (2024)
- [Learning-Based Shielding for Safe Autonomy under Unknown Dynamics](https://mlsanity.com/paper/2410.07359/) (2024)
- [Verification of Unknown Dynamical Systems via Autoencoder Latent Space](https://mlsanity.com/paper/2512.13593/) (2025)

## Abstract (arXiv)

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.