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

TL;DR

This paper introduces a novel use of binary-tree Gaussian processes for formal verification of stochastic systems, enabling efficient abstraction and robust probability bounds without complex error quantification.

Contribution

It leverages the natural abstraction of BTGPs to construct interval Markov chain models, simplifying verification and providing robust probability bounds under uncertainty.

Findings

Achieves polynomial speedup in model construction compared to existing methods.

Provides a unified error quantification formula applicable even outside the BTGP function space.

Enables robust probability bounds for reachability specifications 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.