Pushdown Multi-Agent System Verification

In this paper we investigate the model-checking problem of pushdown multi-agent systems for ATL? specifications. To this aim, we introduce pushdown game structures over which ATL? formulas are interpreted. We show an algorithm that solves the addressed model-checking problem in 3EXPTIME. We also provide a 2EXPSPACE lower bound by showing a reduction from the word acceptance problem for deterministic Turing machines with doubly exponential space.

Authors

• Aniello Murano University of Naples Federico II
• Giuseppe Perelli Sapienza University of Rome

Keywords

No keywords are indexed for this paper.