Formal Verification of Unknown Stochastic Systems via Non-parametric Estimation
<|reference_start|>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.<|reference_end|>
@article{zhang2024formal,
    title={Formal Verification of Unknown Stochastic Systems via Non-parametric
  Estimation},
    author={Zhi Zhang, Chenyu Ma, Saleh Soudijani, Sadegh Soudjani},
    journal={arXiv preprint arXiv:2403.05350},
    year={2024},
    archivePrefix={arXiv},
    eprint={2403.05350},
    primaryClass={eess.SY cs.SY}
}