轮转式概率实时博弈的验证与控制
计算机科学中的逻辑
2019-07-18 v3
摘要
定量验证技术已发展为用于多种形式概率模型的正式分析，如马尔可夫链、马尔可夫决策过程及其变体。它们可用于对系统行为的定量方面（例如安全性、可靠性与性能）提供保证，或辅助合成确保此类保证得以满足的控制器。我们提出轮转式概率定时多人博弈模型，其融合了概率选择、实时时钟与多参与者间的非确定性行为。基于概率定时自动机这一较简模型的数字化时钟方法，我们展示如何计算定量验证的关键度量，即到达目标的概率与期望累积代价。我们在计算机安全与任务调度的案例研究中予以说明。
引用
@article{arxiv.1906.09142,
title = {Verification and Control of Turn-Based Probabilistic Real-Time Games},
author = {Marta Kwiatkowska and Gethin Norman and David Parker},
journal= {arXiv preprint arXiv:1906.09142},
year = {2019}
}