用于随机系统验证的鲁棒完备有限状态抽象
概率论
2022-05-05 v1
摘要
本文关注由非线性随机差分方程建模的离散时间随机系统，并提出用于验证概率线性时序规约的鲁棒抽象。现有文献侧重于为无扰动的随机动态开发可靠抽象技术。然而，迄今为止的可靠性仅针对保留某类时序逻辑规约的满足概率得到证明。我们给出用于验证更一般非线性随机系统的一般 ω-正则线性时间性质概率满足性的构造性有限状态抽象。我们不施加稳定性假设，而是从概率测度可度量空间的拓扑视角分析概率性质。此类抽象既可靠又近似完备。即，给定具体离散时间随机系统及该系统的任意小 L1-扰动，存在一族有限状态马尔可夫链，其满足概率集合包含原系统的满足概率集合，同时被轻微扰动系统的满足概率集合所包含。一个直接结论是，给定概率线性时间规约，在抽象系统的胜/负区域内初始化可保证原系统的满足/不满足。我们提出一个有趣的观察：与确定性情形不同，点质量（狄拉克）扰动无法实现鲁棒完备性。
引用
@article{arxiv.2205.01854,
title = {Robustly Complete Finite-State Abstractions for Verification of Stochastic Systems},
author = {Yiming Meng and Jun Liu},
journal= {arXiv preprint arXiv:2205.01854},
year = {2022}
}