一句话：确定了下推多智能体系统对 ATL 与 ATL* 的模块检查复杂度，分别为 2EXPTIME 完全与 4EXPTIME 完全。
本文研究下推多智能体系统（PMS）在 ATL 和 ATL* 规约下的模块检查问题。作者通过复杂度理论分析建立了判定问题的复杂度上下界，并与已有结果进行比较。主要结论是：对阵 ATL，PMS 的模块检查是 2EXPTIME 完全的，与 CTL 下推模块检查复杂度相同；对阵 ATL*，PMS 的模块检查是 4EXPTIME 完全的，因此比 CTL* 下推模块检查和 PMS 的 ATL* 模型检查都指数级更难。该 ATL* 结果是三指数时间以上但仍属初等复杂度的自然判定问题的罕见例子。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2003-04728,
title = {Module checking of pushdown multi-agent systems},
author = {Laura Bozzelli and Aniello Murano and Adriano Peron},
journal = {Logical Methods in Computer Science},
volume = {Volume 22, Issue 1},
year = {2026},
doi = {10.46298/lmcs-22(1:13)2026}
}