# Data-Driven Abstractions via Binary-Tree Gaussian Processes for Formal Verification

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 27 of its 38 references that are in the map.
- First posted on arXiv 15 Jul 2024.

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

- [On Kernelized Multi-armed Bandits](https://mlsanity.com/paper/1704.00445/) (2017)
- [Gaussian Processes and Kernel Methods: A Review on Connections and Equivalences](https://mlsanity.com/paper/1807.02582/) (2018)
- [Practical and Rigorous Uncertainty Bounds for Gaussian Process Regression](https://mlsanity.com/paper/2105.02796/) (2021)
- [Formal Synthesis of Stochastic Systems via Control Barrier Certificates](https://mlsanity.com/paper/1905.04585/) (2019)
- [Logically-Constrained Neural Fitted Q-Iteration](https://mlsanity.com/paper/1809.07823/) (2018)
- [Data-driven verification and synthesis of stochastic systems via barrier certificates](https://mlsanity.com/paper/2111.10330/) (2021)
- [Sampling-based Reachability Analysis: A Random Set Theory Approach with Adversarial Sampling](https://mlsanity.com/paper/2008.10180/) (2020)
- [Probabilities Are Not Enough: Formal Controller Synthesis for Stochastic Dynamical Models with Epistemic Uncertainty](https://mlsanity.com/paper/2210.05989/) (2022)
- [Neural Abstractions](https://mlsanity.com/paper/2301.11683/) (2023)
- [Safety Verification of Unknown Dynamical Systems via Gaussian Process Regression](https://mlsanity.com/paper/2004.01821/) (2020)
- [Interval Reachability of Nonlinear Dynamical Systems with Neural Network Controllers](https://mlsanity.com/paper/2301.07912/) (2023)
- [Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings](https://mlsanity.com/paper/2403.10497/) (2024)
- [Formal Policy Synthesis for Continuous-Space Systems via Reinforcement Learning](https://mlsanity.com/paper/2005.01319/) (2020)
- [Data-Driven Abstraction-Based Control Synthesis](https://mlsanity.com/paper/2206.08069/) (2022)
- [Formal Control Synthesis for Stochastic Neural Network Dynamic Models](https://mlsanity.com/paper/2203.05903/) (2022)
- [Constructing MDP Abstractions Using Data with Formal Guarantees](https://mlsanity.com/paper/2206.14402/) (2022)
- [Robust Control Barrier Functions for Nonlinear Control Systems with Uncertainty: A Duality-based Approach](https://mlsanity.com/paper/2208.05955/) (2022)
- [Data-Driven Chance Constrained Control using Kernel Distribution Embeddings](https://mlsanity.com/paper/2202.04193/) (2022)
- [Bayesian Formal Synthesis of Unknown Systems via Robust Simulation Relations](https://mlsanity.com/paper/2304.07428/) (2023)
- [Robust Dynamic Programming for Temporal Logic Control of Stochastic Systems](https://mlsanity.com/paper/1811.11445/) (2018)
- [Unmatched Control Barrier Functions: Certainty Equivalence Adaptive Safety](https://mlsanity.com/paper/2207.13873/) (2022)
- [Log-Linear-Time Gaussian Processes Using Binary Tree Kernels](https://mlsanity.com/paper/2210.01633/) (2022)
- [Assume-Guarantee Reinforcement Learning](https://mlsanity.com/paper/2312.09938/) (2023)
- [Contraction-Guided Adaptive Partitioning for Reachability Analysis of Neural Network Controlled Systems](https://mlsanity.com/paper/2304.03671/) (2023)
- [Forward Invariance in Neural Network Controlled Systems](https://mlsanity.com/paper/2309.09043/) (2023)
- [Formal Verification of Unknown Stochastic Systems via Non-parametric Estimation](https://mlsanity.com/paper/2403.05350/) (2024)
- [Safe Learning for Uncertainty-Aware Planning via Interval MDP Abstraction](https://mlsanity.com/paper/2202.01358/) (2022)

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

- [Average Reward Reinforcement Learning for Omega-Regular and Mean-Payoff Objectives](https://mlsanity.com/paper/2505.15693/) (2025)
- [Kernel-Based Learning of Safety Barriers](https://mlsanity.com/paper/2601.12002/) (2026)
- [Safety Certification is Classification](https://mlsanity.com/paper/2605.06087/) (2026)

## Abstract (arXiv)

To advance formal verification of stochastic systems against temporal logic requirements for handling unknown dynamics, researchers have been designing data-driven approaches inspired by breakthroughs in the underlying machine learning techniques. As one promising research direction, abstraction-based solutions based on Gaussian process (GP) regression have become popular for their ability to learn a representation of the latent system from data with a quantified error. Results obtained based on this model are then translated to the true system via various methods. In a recent publication, GPs using a so-called binary-tree kernel have demonstrated a polynomial speedup w.r.t. the size of the data compared to their vanilla version, outcompeting all existing sparse GP approximations. Incidentally, the resulting binary-tree Gaussian process (BTGP) is characteristic for its piecewise-constant posterior mean and covariance functions, naturally abstracting the input space into discrete partitions. In this paper, we leverage this natural abstraction of the BTGP for formal verification, eliminating the need for cumbersome abstraction and error quantification procedures. We show that the BTGP allows us to construct an interval Markov chain model of the unknown system with a speedup that is polynomial w.r.t. the size of the abstraction compared to alternative approaches. We provide a delocalized error quantification via a unified formula even when the true dynamics do not live in the function space of the BTGP. This allows us to compute upper and lower bounds on the probability of satisfying reachability specifications that are robust to both aleatoric and epistemic uncertainties.