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

TL;DR

This work tackles the problem of formally verifying stochastic systems with unknown dynamics against infinite-horizon reachability specifications. It leverages binary-tree Gaussian processes (BTGPs) with a discontinuous binary-tree kernel to learn a piecewise-constant, finite-state abstraction of the latent dynamics, enabling an interval Markov chain (IMC) that captures both stochastic and epistemic uncertainties. A delocalized, piecewise-constant error bound is derived, guaranteeing that the BTGP-based abstraction bounds the true dynamics even when the true function lies outside the BTGP RKHS via a misspecified-kernel analysis. Verification is performed via an interval iteration algorithm on the IMC, yielding robust lower/upper bounds on the satisfaction probability with polynomial speedups in the abstraction size relative to traditional GP-based approaches. The case study demonstrates practical gains, producing rapid abstraction and verification while maintaining guarantees on system behavior under uncertainty.

Abstract

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.

Figures (4)

• Figure 1: The BTGP contains functions that are piecewise constant over the partitions of ${\mathbb{X}}$. The posterior mean $\hat{\mu}_N$ and double standard deviation $\hat{\mu}_N\pm 2\hat{\sigma}_N$ are displayed as a piecewise-constant graph and an area plot in light blue, respectively. For this example with chosen precision $q=2$, the posterior mean takes values $\hat{\mu}_N\in\{y_{s_0},\ldots,y_{s_3}\}$.
• Figure 2: Computing transition probabilities from a continuous GP (top) vs. from a BTGP (bottom).
• Figure 3: Lower bound on the infinite-horizon reachability probability as a function of the initial state.
• Figure 4: BTGP model fit $\hat{\mu}_{d, N}(x)\pm 3\hat{\sigma}_{d, N}(x)$ versus $f_d(x)$ (top: $d=1$, bottom: $d=2$).

Theorems & Definitions (14)

• Remark 1
• Definition 1: Gaussian process (GP)
• Definition 2: Posterior GP
• Definition 3: Binary-tree (BT) kernel
• Remark 2
• Remark 3
• Theorem 1: BT function space
• Corollary 1: BT RKHS norm bound
• Theorem 2: Piecewise-constant error bound
• Remark 4: Approximating a continuous kernel