Safety Verification of Stochastic Systems under Signal Temporal Logic Specifications
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909528626298880 |
|---|---|
| author | Ma, Liqian Liu, Zishun Yu, Hongzhe Chen, Yongxin |
| author_facet | Ma, Liqian Liu, Zishun Yu, Hongzhe Chen, Yongxin |
| contents | We study the verification problem of stochastic systems under signal temporal logic (STL) specifications. We propose a novel approach that enables the verification of the probabilistic satisfaction of STL specifications for nonlinear systems subject to both bounded deterministic disturbances and stochastic disturbances. Our method, referred to as the STL erosion strategy, reduces the probabilistic verification problem into a deterministic verification problem with a tighter STL specification. The degree of tightening is determined by leveraging recent results on bounding the deviation between the stochastic trajectory and the deterministic trajectory. Our approach can be seamlessly integrated with any existing deterministic STL verification algorithm. Numerical experiments are conducted to showcase the efficacy of our method. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2503_04762 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Safety Verification of Stochastic Systems under Signal Temporal Logic Specifications Ma, Liqian Liu, Zishun Yu, Hongzhe Chen, Yongxin Logic in Computer Science Formal Languages and Automata Theory Systems and Control We study the verification problem of stochastic systems under signal temporal logic (STL) specifications. We propose a novel approach that enables the verification of the probabilistic satisfaction of STL specifications for nonlinear systems subject to both bounded deterministic disturbances and stochastic disturbances. Our method, referred to as the STL erosion strategy, reduces the probabilistic verification problem into a deterministic verification problem with a tighter STL specification. The degree of tightening is determined by leveraging recent results on bounding the deviation between the stochastic trajectory and the deterministic trajectory. Our approach can be seamlessly integrated with any existing deterministic STL verification algorithm. Numerical experiments are conducted to showcase the efficacy of our method. |
| title | Safety Verification of Stochastic Systems under Signal Temporal Logic Specifications |
| topic | Logic in Computer Science Formal Languages and Automata Theory Systems and Control |
| url | https://arxiv.org/abs/2503.04762 |