基于障碍证书的切换随机系统验证
计算机科学中的逻辑
2021-09-28 v1 系统与控制
系统与控制
摘要
本文提出了一种针对连续时间切换随机系统的时间逻辑验证方法。我们的目标是求出在有限时间范围内满足复杂时序属性的概率下界。系统所需的时序属性使用一种称为 safe-LTL 的线性时序逻辑片段来表达，该片段针对有限迹。我们的方法结合了基于自动机的验证与障碍证书的使用。它依赖于将与规约之否定相关联的自动机分解为一系列更简单的可达性任务，并通过公共或多重障碍证书计算这些可达性概率的上界。理论结果通过应用反例引导归纳综合框架来寻找障碍证书加以说明。
引用
@article{arxiv.2109.12420,
title = {Verification of Switched Stochastic Systems via Barrier Certificates},
author = {Mahathi Anand and Pushpak Jagtap and Majid Zamani},
journal= {arXiv preprint arXiv:2109.12420},
year = {2021}
}
备注
arXiv admin note: substantial text overlap with arXiv:1807.00064