Formal Verification of Unknown Stochastic Systems via Non-parametric Estimation

Zhi Zhang, Chenyu Ma, Saleh Soudijani, Sadegh Soudjani
Proceedings of The 27th International Conference on Artificial Intelligence and Statistics, PMLR 238:3277-3285, 2024.

Abstract

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.

Cite this Paper

BibTeX
@InProceedings{pmlr-v238-zhang24i, title = {Formal Verification of Unknown Stochastic Systems via Non-parametric Estimation}, author = {Zhang, Zhi and Ma, Chenyu and Soudijani, Saleh and Soudjani, Sadegh}, booktitle = {Proceedings of The 27th International Conference on Artificial Intelligence and Statistics}, pages = {3277--3285}, year = {2024}, editor = {Dasgupta, Sanjoy and Mandt, Stephan and Li, Yingzhen}, volume = {238}, series = {Proceedings of Machine Learning Research}, month = {02--04 May}, publisher = {PMLR}, pdf = {https://proceedings.mlr.press/v238/zhang24i/zhang24i.pdf}, url = {https://proceedings.mlr.press/v238/zhang24i.html}, abstract = {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.} }
Endnote
%0 Conference Paper %T Formal Verification of Unknown Stochastic Systems via Non-parametric Estimation %A Zhi Zhang %A Chenyu Ma %A Saleh Soudijani %A Sadegh Soudjani %B Proceedings of The 27th International Conference on Artificial Intelligence and Statistics %C Proceedings of Machine Learning Research %D 2024 %E Sanjoy Dasgupta %E Stephan Mandt %E Yingzhen Li %F pmlr-v238-zhang24i %I PMLR %P 3277--3285 %U https://proceedings.mlr.press/v238/zhang24i.html %V 238 %X 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.
APA
Zhang, Z., Ma, C., Soudijani, S. & Soudjani, S.. (2024). Formal Verification of Unknown Stochastic Systems via Non-parametric Estimation. Proceedings of The 27th International Conference on Artificial Intelligence and Statistics, in Proceedings of Machine Learning Research 238:3277-3285 Available from https://proceedings.mlr.press/v238/zhang24i.html.

Related Material