mlsanityData to 7 Oct 2026

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

arXiv 2407.21029 ↗First posted 15 Jul 2024cs.LO cs.FL cs.LGcited by 3

Not on the map. Why?

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.

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

Builds on

27 of 38 references.

References · 27

  1. 2017On Kernelized Multi-armed Banditscited by 348
  2. 2018Gaussian Processes and Kernel Methods: A Review on Connections and Equivalencescited by 188
  3. 2021Practical and Rigorous Uncertainty Bounds for Gaussian Process Regressioncited by 49
  4. 2019Formal Synthesis of Stochastic Systems via Control Barrier Certificatescited by 21
  5. 2018Logically-Constrained Neural Fitted Q-Iterationcited by 17
  6. 2021Data-driven verification and synthesis of stochastic systems via barrier certificatescited by 12
  7. 2020Sampling-based Reachability Analysis: A Random Set Theory Approach with Adversarial Samplingcited by 11
  8. 2022Probabilities Are Not Enough: Formal Controller Synthesis for Stochastic Dynamical Models with Epistemic Uncertaintycited by 11
  9. 2023Neural Abstractionscited by 11
  10. 2020Safety Verification of Unknown Dynamical Systems via Gaussian Process Regressioncited by 9
  11. 2024Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddingscited by 9
  12. 2020Formal Policy Synthesis for Continuous-Space Systems via Reinforcement Learningcited by 8
15 more
  1. 2023Interval Reachability of Nonlinear Dynamical Systems with Neural Network Controllerscited by 8
  2. 2022Formal Control Synthesis for Stochastic Neural Network Dynamic Modelscited by 7
  3. 2022Data-Driven Abstraction-Based Control Synthesiscited by 7
  4. 2022Constructing MDP Abstractions Using Data with Formal Guaranteescited by 7
  5. 2022Data-Driven Chance Constrained Control using Kernel Distribution Embeddingscited by 5
  6. 2022Robust Control Barrier Functions for Nonlinear Control Systems with Uncertainty: A Duality-based Approachcited by 5
  7. 2023Bayesian Formal Synthesis of Unknown Systems via Robust Simulation Relationscited by 5
  8. 2018Robust Dynamic Programming for Temporal Logic Control of Stochastic Systemscited by 4
  9. 2022Unmatched Control Barrier Functions: Certainty Equivalence Adaptive Safetycited by 4
  10. 2022Log-Linear-Time Gaussian Processes Using Binary Tree Kernelscited by 4
  11. 2023Assume-Guarantee Reinforcement Learningcited by 4
  12. 2023Contraction-Guided Adaptive Partitioning for Reachability Analysis of Neural Network Controlled Systemscited by 3
  13. 2024Formal Verification of Unknown Stochastic Systems via Non-parametric Estimationcited by 3
  14. 2022Safe Learning for Uncertainty-Aware Planning via Interval MDP Abstractioncited by 2
  15. 2023Forward Invariance in Neural Network Controlled Systemscited by 2

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2025: 1; 2026: 2.

3 papers.

  1. 2025Average Reward Reinforcement Learning for Omega-Regular and Mean-Payoff Objectivescited by 0
  2. 2026Kernel-Based Learning of Safety Barrierscited by 0
  3. 2026Safety Certification is Classificationcited by 0