论文标题
倒数多代理系统的模块检查
Module checking of pushdown multi-agent systems
论文作者
论文摘要
在本文中，我们研究了针对ATL和ATL*规范的下降多代理系统（PMS）的模块检查问题。我们确定对于ATL，PMS的模块检查是2Exptime-Complete，这与CTL的下降模块检查相同。另一方面，我们表明，PMS的ATL*模块检查是4Exptime-Complete，因此比CTL* PUSHDown Module-Checking和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.
