Pushdown multi-agent system verification
Aniello Murano, Giuseppe Perelli · 2015
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 algo-rithm that solves the addressed model-checking problem in 3ExpTime. We also provide a 2ExpSpace lower bound by showing a reduc-tion from the word acceptance problem for de-terministic Turing machines with doubly expo-nential space. 1