关于策略推理：模型检测问题研究
计算机科学中的逻辑
2014-02-13 v2 多智能体系统
逻辑
摘要
在开放系统验证中，为了正式检查可靠性，需要适当的模型来描述智能体之间的交互，并表达系统无论环境如何行为时的正确性。在此背景下，一个重要的贡献是在多智能体博弈的设定中，针对策略能力的模态逻辑，如ATL、ATL*等。最近，Chatterjee、Henzinger和Piterman引入了策略逻辑（此处记为CHP-SL），旨在获得一个用于显式推理策略的强大框架。CHP-SL通过使用策略上的一阶量化得到，并在双智能体回合制博弈这一非常特定的设定中进行了研究，其中给出了一个非初等模型检测算法。虽然CHP-SL是一种表达能力很强的逻辑，但我们认为它并未完全捕捉多智能体系统的策略方面。在本文中，我们引入并研究了一种更通用的策略逻辑（记为SL），用于在多智能体并发博弈中推理策略。我们证明SL包含CHP-SL，同时保持可判定的模型检测问题。特别地，我们提出的算法在计算上并不比已知的CHP-SL最佳算法更困难。此外，我们证明SL的模型检测问题是NonElementarySpace-hard的。这一负面结果促使我们在此研究SL的语法片段，这些片段严格包含ATL*，以期获得初等模型检测问题。其中，我们研究了子逻辑SL[NG]、SL[BG]和SL[1G]。它们分别包含具有嵌套时间目标、目标的布尔组合以及每次单个目标的特殊前束范式的公式。关于这些逻辑，我们证明SL[1G]的模型检测问题是2ExpTime-complete，因此并不比ATL*的模型检测问题更困难。
引用
@article{arxiv.1112.6275,
title = {Reasoning About Strategies: On the Model-Checking Problem},
author = {Fabio Mogavero and Aniello Murano and Giuseppe Perelli and Moshe Y. Vardi},
journal= {arXiv preprint arXiv:1112.6275},
year = {2014}
}