Data-Driven Abstractions via Binary-Tree Gaussian Processes for Formal Verification
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.
Code (0)
등록된 구현이 없습니다.
Tasks
Gaussian ProcessesMethods 이 논문이 사용한 방법론
Similar Papers 제목 키워드 기반
Log-Linear-Time Gaussian Processes Using Binary Tree Kernels
Gaussian processes (GPs) produce good probabilistic models of functions, but most GP kernels require $O((n+m)n^2)$ time, where $n$ is the number of data points and $m$ the number of predictive locations. We present a new…
Gaussian ProcessesregressionRobust estimation of tree structured models
Consider the problem of learning undirected graphical models on trees from corrupted data. Recently Katiyar et al. showed that it is possible to recover trees from noisy binary data up to a small equivalence class of pos…
Q-Search Trees: An Information-Theoretic Approach Towards Hierarchical Abstractions for Agents with Computational Limitations
In this paper, we develop a framework to obtain graph abstractions for decision-making by an agent where the abstractions emerge as a function of the agent's limited computational resources. We discuss the connection of …
Decision MakingA Linear Programming Approach for Resource-Aware Information-Theoretic Tree Abstractions
In this chapter, an integer linear programming formulation for the problem of obtaining task-relevant, multi-resolution, environment abstractions for resource-constrained autonomous agents is presented. The formulation l…
Trees as Gaussians: Large-Scale Individual Tree Mapping
Trees are key components of the terrestrial biosphere, playing vital roles in ecosystem function, climate regulation, and the bioeconomy. However, large-scale monitoring of individual trees remains limited by inadequate …