论ATL的表达性和复杂性
On the Expressiveness and Complexity of ATL
摘要：
ATL是面向多代理系统中属性的规范和验证的时态逻辑。它允许的原因上存在的战略联盟的代理人，以执行一个给定的属性。在本文中，我们首先精确地描述了交替迁移系统和并发博弈结构上的ATL模型检测的复杂性时，代理的数量是不固定的。我们证明了它是Δ^P_2 -和Δ ^P_3-。3-完整，取决于底层的多代理模型（分别为ATS和CGS）。我们还考虑了ATL的一些扩展的相同的问题。然后，我们考虑表达问题。我们展示了ATS和CGS是如何相关的，并提供这些模型之间的翻译。交替互模拟我们还证明了ATL的标准定义（建立在模态“Next”，“Always”和“Until”上）不能表达其模态的连续性：有必要明确地添加模态“Release”。
英文摘要：
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. In this paper, we first precisely characterize the complexity of ATL model-checking over Alternating Transition Systems and Concurrent Game Structures when the number of agents is not fixed. We prove that it is Δ^P_2 - and Δ^P_?_3-complete, depending on the underlying multi-agent model (ATS and CGS resp.). We also consider the same problems for some extensions of ATL. We then consider expressiveness issues. We show how ATS and CGS are related and provide translations between these models w.r.t. alternating bisimulation. We also prove that the standard definition of ATL (built on modalities "Next", "Always" and "Until") cannot express the duals of its modalities: it is necessary to explicitely add the modality "Release".
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
