Formal Verification of Unknown Stochastic Systems via Non-parametric Estimation
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 \emph{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^{-\frac{1}{3+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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Data-driven Safety Verification of Stochastic Systems via Barrier Certificates
In this paper, we propose a data-driven approach to formally verify the safety of (potentially) unknown discrete-time continuous-space stochastic systems. The proposed framework is based on a notion of barrier certificat…
Bayesian Formal Synthesis of Unknown Systems via Robust Simulation Relations
This paper addresses the problem of data-driven computation of controllers that are correct by design for safety-critical systems and can provably satisfy (complex) functional requirements. With a focus on continuous-spa…
Conformal Prediction-Based MPC for Stochastic Linear Systems
We propose a stochastic model predictive control (MPC) framework for linear systems subject to joint-in-time chance constraints under unknown disturbance distributions. Unlike existing approaches that rely on parametric …
Tuning Trains Speed in Railway Scheduling
Railway scheduling consists in ensuring that a set of trains evolve in a shared rail network without collisions, while meeting schedule constraints. This problem is notoriously difficult, even more in the case of uncerta…
SchedulingData-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 m…
Gaussian Processes