Module checking of pushdown multi-agent systems

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.