Pushdown Multi-Agent System Verification. Murano, A. and Perelli, G. In Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July25-31, 2015, pages 1090–1097, 2015.
Paper abstract bibtex 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.
@inproceedings
{
C-MP15a,
author = {Aniello Murano and Giuseppe Perelli},
title = {Pushdown Multi-Agent System Verification},
abstract = {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.},
booktitle = {Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, {IJCAI} 2015, Buenos Aires, Argentina, July25-31, 2015},
pages = "1090--1097",
year = "2015",
url = {https://www.ijcai.org/Abstract/15/158},
}