  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.
