Laura Bozzelli ; Aniello Murano ; Adriano Peron - Module checking of pushdown multi-agent systems

lmcs:8458 - Logical Methods in Computer Science, February 17, 2026, Volume 22, Issue 1 - https://doi.org/10.46298/lmcs-22(1:13)2026
Module checking of pushdown multi-agent systemsArticle

Authors: Laura Bozzelli ; Aniello Murano ; Adriano Peron

    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.


    Volume: Volume 22, Issue 1
    Published on: February 17, 2026
    Accepted on: October 26, 2025
    Submitted on: September 8, 2021
    Keywords: Logic in Computer Science, Formal Languages and Automata Theory, Multiagent Systems

    Consultation statistics

    This page has been seen 19 times.
    This article's PDF has been downloaded 5 times.