On the Expressiveness and Complexity of ATL
On the Expressiveness and Complexity of ATL
复制标题
DOI：
10.2168/lmcs-4(2:7)2008
复制
发表时间：
2007-03
期刊：
影响因子：
--
通讯作者：
F. Laroussinie;N. Markey;Ghassan Oreiby
中科院分区：
文献类型：
--
作者：
F. Laroussinie;N. Markey;Ghassan Oreiby
ATL 是一种时态逻辑，旨在指定和验证多代理系统中的属性。它允许对代理联盟策略的存在进行推理，以强制执行给定的财产。我们证明，ATL 的标准定义（建立在模态“Next”、“Always”和“Until”之上）必须完成，以便表达其模态的对偶：有必要添加模态“Release”。然后，我们精确地描述了当智能体数量不固定时 ATL 模型检查的复杂性。我们证明它是 Δ2P 和 Δ3P 完全的，具体取决于底层的多智能体模型（ATS 和 CGS 分别）。我们还证明，即使代理数量固定，ATL+ 模型检查对于两个模型来说都是 Δ3P- 完整的。
ATL is a temporal logic geared towards the specification and verification of properties in multi-agents systems. It allows to reason on the existence of strategies for coalitions of agents in order to enforce a given property. We prove that the standard definition of ATL (built on modalities "Next", "Always" and "Until") has to be completed in order to express the duals of its modalities: it is necessary to add the modality "Release". We then precisely characterize the complexity of ATL model-checking when the number of agents is not fixed. We prove that it is Δ2P - and Δ3P-complete, depending on the underlying multi-agent model (ATS and CGS resp.). We also prove that ATL+ model-checking is Δ3P- complete over both models, even with a fixed number of agents.