Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Module checking of pushdown multi-agent systems

Laura Bozzelli, Aniello Murano, Adriano Peron

TL;DR

The paper resolves the exact complexity of pushdown module-checking for PMS against ATL and ATL*, showing a sharp gap: $2EXPTIME$-complete for ATL and $4EXPTIME$-complete for ATL* (even with a fixed formula for the latter). The authors develop an automata-theoretic framework using parity alternating automata (ACG) and parity nondeterministic pushdown tree automata (NPTA) to obtain the upper bounds, and they prove the $4EXPTIME$-hardness of ATL* pushdown module-checking by a reduction from $3EXPSPACE$-bounded alternating Turing machines (ATM). The key technical contribution is encoding environment strategy trees as labeled trees and reducing PMS reactive satisfaction to emptiness checks of NPTA, carefully handling the interplay between pushdown behavior and environment nondeterminism. These results confirm that pushdown module-checking remains exponentially harder than its finite-state counterpart and highlight the high complexity of strategic reasoning in an infinite-state open system setting.

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.

Module checking of pushdown multi-agent systems

TL;DR

The paper resolves the exact complexity of pushdown module-checking for PMS against ATL and ATL*, showing a sharp gap: -complete for ATL and -complete for ATL* (even with a fixed formula for the latter). The authors develop an automata-theoretic framework using parity alternating automata (ACG) and parity nondeterministic pushdown tree automata (NPTA) to obtain the upper bounds, and they prove the -hardness of ATL* pushdown module-checking by a reduction from -bounded alternating Turing machines (ATM). The key technical contribution is encoding environment strategy trees as labeled trees and reducing PMS reactive satisfaction to emptiness checks of NPTA, carefully handling the interplay between pushdown behavior and environment nondeterminism. These results confirm that pushdown module-checking remains exponentially harder than its finite-state counterpart and highlight the high complexity of strategic reasoning in an infinite-state open system setting.

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.

Paper Structure

This paper contains 31 sections, 10 theorems, 33 equations, 3 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Verification of pushdown systems
  3. Our contribution
  4. Preliminaries
  5. Concurrent game structures ( CGS)
  6. Pushdown multi-agent systems ( PMS)
  7. The logics ATL* and ATL
  8. ATL* and ATL Pushdown Module-checking
  9. Pushdown Module-checking
  10. Decision procedures
  11. Parity NPTA KPV02
  12. Parity alternating automata for CGS (parity ACG) ScheweF06
  13. From ATL$^{*}$ and ATL to parity ACG
  14. Upper bounds for ATL and ATL* pushdown module-checking
  15. Encoding of environment strategy trees of open $\text{\sffamily PMS}$
  16. ...and 16 more sections

Key Result

Proposition 3.1

KPV02Bozzelli10pushdown The emptiness problem for a parity NPTA of index $m$ with $n$ states and transition function $\rho$ can be solved in time $O(|\rho|\cdot 2^{O(||\rho||^2\cdot n^2\cdot m^2 \log m)})$.

Figures (3)

  • Figure 1: Multi-agent pushdown coffee machine ${\mathcal{S}}_{cof}$
  • Figure 2: Subtree of the unwinding ${\textit{Unw}}({\mathcal{G}}({\mathcal{S}}))$ of the open $\text{\sffamily PMS}$${\mathcal{S}}$ rooted at an $acc$-node (pop-phase)
  • Figure 3: Marked copies of $2$-blocks in the pop-phase of the open $\text{\sffamily PMS}$${\mathcal{S}}$

Theorems & Definitions (21)

  • Definition 2.1: CGS
  • Definition 2.2
  • Definition 2.3
  • Definition 2.4: Open CGS
  • Example 2.5
  • Proposition 3.1
  • Theorem 3.2
  • Theorem 3.3
  • Corollary 3.4
  • Theorem 3.5
  • ...and 11 more