Module checking of pushdown multi-agent systems
Logic in Computer Science
2026-03-11 v6 Formal Languages and Automata Theory
Multiagent Systems
Abstract
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.
Cite
@article{arxiv.2003.04728,
title = {Module checking of pushdown multi-agent systems},
author = {Laura Bozzelli and Aniello Murano and Adriano Peron},
journal= {arXiv preprint arXiv:2003.04728},
year = {2026}
}