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.
Pushdown multi-agent system verification / Murano, A.; Perelli, G.. - In: IJCAI. - ISSN 1045-0823. - 2015:(2015), pp. 1090-1097. (Intervento presentato al convegno 24th International Joint Conference on Artificial Intelligence, IJCAI 2015 tenutosi a Buenos Aires; Argentina).
Pushdown multi-agent system verification
Perelli G.
2015
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.| File | Dimensione | Formato | |
|---|---|---|---|
|
Murano_Pushdown_2015.pdf
solo gestori archivio
Tipologia:
Versione editoriale (versione pubblicata con il layout dell'editore)
Licenza:
Tutti i diritti riservati (All rights reserved)
Dimensione
488.42 kB
Formato
Adobe PDF
|
488.42 kB | Adobe PDF | Contatta l'autore |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
