In this paper, we investigate the module-checking problem of pushdown multi-agent systems (PMS) against ATL and ATL* specifications. We establish that for ATL, module checking of PMS is 2EXPTIME-complete, which is the same complexity as pushdown module-checking for CTL. On the other hand, we show that ATL* module-checking of PMS turns out to be 4EXPTIME-complete, hence exponentially harder than both CTL* pushdown module-checking and ATL* model-checking of PMS. Our result for ATL* provides a rare example of a natural decision problem that is elementary yet but with a complexity that is higher than triply exponential-time.

翻译：本文研究了下推多智能体系统（PMS）针对ATL与ATL*规范的模块检测问题。我们证明，对于ATL而言，PMS的模块检测是2EXPTIME完全的，其复杂度与CTL的下推模块检测相同。另一方面，我们表明PMS的ATL*模块检测是4EXPTIME完全的，因此比CTL*下推模块检测以及PMS的ATL*模型检测均指数级更难。我们关于ATL*的结果提供了一个罕见的例子：一个自然的判定问题是初等的，但其复杂度却高于三重指数时间。