Statistical verification of PCTL using antithetic and stratified samples
Statistical verification of PCTL using antithetic and stratified samples
复制标题
DOI：
10.1007/s10703-019-00339-8
复制
发表时间：
2019-11-01
影响因子：
0.8
通讯作者：
Dullerud, Geir E.
中科院分区：
文献类型：
--
作者：
Wang, Yu;Roohi, Nima;Dullerud, Geir E.
在这项工作中，我们研究了具有分层和对立样本的离散时间马尔可夫链（dtmc）上概率计算树逻辑（PCTL）公式的统计验证问题。我们表明，通过正确选择dtmc的表示，可以通过分层或反采样技术为一小部分PCTL公式生成语义负相关的样本。使用分层或对立样本，我们提出了基于顺序概率比检验的具有渐近正确性保证的统计验证算法，并表明这些算法比使用独立蒙特卡罗抽样的算法更具样本效率。最后，通过多个基准的数值实验，验证了分层和对立样本统计验证算法的有效性。
In this work, we study the problem of statistically verifying Probabilistic Computation Tree Logic (PCTL) formulas on discrete-time Markov chains (DTMCs) with stratified and antithetic samples. We show that by properly choosing the representation of the DTMCs, semantically negatively correlated samples can be generated for a fraction of PCTL formulas via the stratified or antithetic sampling techniques. Using stratified or antithetic samples, we propose statistical verification algorithms with asymptotic correctness guarantees based on sequential probability ratio tests, and show that these algorithms are more sample-efficient than the algorithms using independent Monte Carlo sampling. Finally, the efficiency of the statistical verification algorithm with stratified and antithetic samples is demonstrated by numerical experiments on several benchmarks.