  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.
