  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.
