回合制随机博弈的符号化验证与策略综合
计算机科学中的逻辑
2022-11-14 v1
摘要
随机博弈是一种方便的建模形式，用于描述在不确定环境中相互竞争或协作的理性智能体系统。针对此类模型的的概率模型检验技术，使我们能够正式指定集体或个体行为的定量规约，并自动综合出保证满足这些规约的智能体策略。尽管在算法与工具支持方面已取得良好进展，效率与可扩展性仍是挑战。本文研究基于多终端二元决策图的符号化实现。我们描述了如何针对基于零和或纳什均衡的时序逻辑规约，构建并验证回合制随机博弈。我们为此类博弈整理了一组基准，并评估了我们方法的性能，表明其在若干情况下更优，且以符号化方式综合的策略可显著更紧凑。
引用
@article{arxiv.2211.06141,
title = {Symbolic Verification and Strategy Synthesis for Turn-based Stochastic Games},
author = {Marta Kwiatkowska and Gethin Norman and David Parker and Gabriel Santos},
journal= {arXiv preprint arXiv:2211.06141},
year = {2022}
}