# Formal Verification of Unknown Stochastic Systems via Non-parametric Estimation

arXiv: https://arxiv.org/abs/2403.05350 · HTML: https://mlsanity.com/paper/2403.05350/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 8 Mar 2024.

## Built on by (most cited first, 3 of 3)

- [Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings](https://mlsanity.com/paper/2403.10497/) (2024)
- [Data-Driven Abstractions via Binary-Tree Gaussian Processes for Formal Verification](https://mlsanity.com/paper/2407.21029/) (2024)
- [Kernel-Based Learning of Safety Barriers](https://mlsanity.com/paper/2601.12002/) (2026)

## Abstract (arXiv)

A novel data-driven method for formal verification is proposed to study complex systems operating in safety-critical domains. The proposed approach is able to formally verify discrete-time stochastic dynamical systems against temporal logic specifications only using observation samples and without the knowledge of the model, and provide a probabilistic guarantee on the satisfaction of the specification. We first propose the theoretical results for using non-parametric estimation to estimate an asymptotic upper bound for the Lipschitz constant of the stochastic system, which can determine a finite abstraction of the system. Our results prove that the asymptotic convergence rate of the estimation is O(n^-frac13+d), where d is the dimension of the system and n is the data scale. We then construct interval Markov decision processes using two different data-driven methods, namely non-parametric estimation and empirical estimation of transition probabilities, to perform formal verification against a given temporal logic specification. Multiple case studies are presented to validate the effectiveness of the proposed methods.