# Safety Verification of Unknown Dynamical Systems via Gaussian Process Regression

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

## Key facts

- Cited by 9 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 4 Apr 2020.

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

- [Probabilities Are Not Enough: Formal Controller Synthesis for Stochastic Dynamical Models with Epistemic Uncertainty](https://mlsanity.com/paper/2210.05989/) (2022)
- [Certification of Iterative Predictions in Bayesian Neural Networks](https://mlsanity.com/paper/2105.10134/) (2021)
- [Formal Verification of Unknown Dynamical Systems via Gaussian Process Regression](https://mlsanity.com/paper/2201.00655/) (2021)
- [Probabilistic Reach-Avoid for Bayesian Neural Networks](https://mlsanity.com/paper/2310.01951/) (2023)
- [Data-Driven Abstractions via Binary-Tree Gaussian Processes for Formal Verification](https://mlsanity.com/paper/2407.21029/) (2024)
- [Barrier Certificates for Unknown Systems with Latent States and Polynomial Dynamics using Bayesian Inference](https://mlsanity.com/paper/2504.01807/) (2025)
- [TubeDAgger: Reducing the Number of Expert Interventions with Stochastic Reach-Tubes](https://mlsanity.com/paper/2510.00906/) (2025)
- [Conformal Reachability for Safe Control in Unknown Environments](https://mlsanity.com/paper/2602.03799/) (2026)
- [Scenario Generation for Risk-Aware Reinforcement Learning with Probably Approximately Safe Guarantees](https://mlsanity.com/paper/2606.04812/) (2026)

## Abstract (arXiv)

The deployment of autonomous systems that operate in unstructured environments necessitates algorithms to verify their safety. This can be challenging due to, e.g., black-box components in the control software, or undermodelled dynamics that prevent model-based verification. We present a novel verification framework for an unknown dynamical system from a given set of noisy observations of the dynamics. Using Gaussian processes trained on this data set, the framework abstracts the system as an uncertain Markov process with discrete states defined over the safe set. The transition bounds of the abstraction are derived from the probabilistic error bounds between the regression and underlying system. An existing approach for verifying safety properties over uncertain Markov processes then generates safety guarantees. We demonstrate the versatility of the framework on several examples, including switched and nonlinear systems.