解决多智能体系统在不确定环境下的可靠性验证难题。
Robust Verification of Concurrent Stochastic Games
- 引入鲁棒随机博弈模型，用区间概率刻画转移不确定性
- 支持有限与无限时域的零和及非零和博弈验证
- 在大型基准测试中验证了方法的有效性，适合安全关键系统研究者
自主系统常在多智能体环境中运行，需在不确定条件下做出并发战略决策。传统并发随机博弈（CSG）要求精确指定转移概率，这在许多真实场景中不切实际。本文提出鲁棒CSG及其子类区间CSG（ICSG），用于建模对转移概率的信念不确定性。针对最坏情况下的不确定性假设，提出全新的鲁棒验证框架，涵盖有限与无限时域目标，适用于零和与非零和情形（后者基于社会福利最优的纳什均衡）。构建了基于PRISM-games的实现，并在多个大型基准上展示了对ICSG进行鲁棒验证的可行性。
原文摘要 · Abstract (English)
Autonomous systems often operate in multi-agent settings and need to make concurrent, strategic decisions, typically in uncertain environments. Verification and control problems for these systems can be tackled with concurrent stochastic games (CSGs), but this model requires transition probabilities to be precisely specified - an unrealistic requirement in many real-world settings. We introduce *robust CSGs* and their subclass *interval CSGs* (ICSGs), which capture epistemic uncertainty about transition probabilities in CSGs. We propose a novel framework for *robust* verification of these models under worst-case assumptions about transition uncertainty. Specifically, we develop the underlying theoretical foundations and efficient algorithms, for finite- and infinite-horizon objectives in both zero-sum and nonzero-sum settings, the latter based on (social-welfare optimal) Nash equilibria. We build an implementation in the PRISM-games model checker and demonstrate the feasibility of robust verification of ICSGs across a selection of large benchmarks.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。