ATL Satisfiability is Indeed EXPTIME-complete
ATL Satisfiability is Indeed EXPTIME-complete
复制标题
DOI：
10.1093/logcom/exl009
复制
发表时间：
2006-12
期刊：
影响因子：
--
通讯作者：
Dirk Walther;C. Lutz;F. Wolter;M. Wooldridge
中科院分区：
文献类型：
--
作者：
Dirk Walther;C. Lutz;F. Wolter;M. Wooldridge
Alternating-time Temporal Logic（ATL）在开放分布式系统和类游戏多智能体系统的规范和验证中得到越来越广泛的应用。本文研究了ATL可满足性问题的计算复杂性。对于代理集合预先固定的情况，这个问题在货车德里梅伦的结果中以ExpTime-complete解决。如果代理的集合不是预先固定的，那么货车德里梅伦的构造产生2 ExpTime上界。在本文中，我们专注于后者的情况下，并定义了三个自然变化的可满足性问题。虽然这些变化都没有预先修复代理的集合，但我们能够通过类型消除构造来证明ExpTime中所有代理的包容性，从而将现有的2 ExpTime上限提高到紧ExpTime上限。
The Alternating-time Temporal Logic (ATL) of Alur, Henzinger, and Kupferman is being increasingly widely applied in the specification and verification of open distributed systems and game-like multi-agent systems. In this paper, we investigate the computational complexity of the satisfiability problem for ATL. For the case where the set of agents is fixed in advance, this problem was settled at ExpTime-complete in a result of van Drimmelen. If the set of agents is not fixed in advance, then van Drimmelen’s construction yields a 2ExpTime upper bound. In this paper, we focus on the latter case and define three natural variations of the satisfiability problem. Although none of these variations fixes the set of agents in advance, we are able to prove containment in ExpTime for all of them by means of a type elimination construction—thus improving the existing 2ExpTime upper bound to a tight ExpTime one.