Alternating-Time Temporal Logic (ATL∗) is a central logic for multiagent systems. Its extension to the imperfect information setting (ATLJ) is well known to have an undecidable model-checking problem when agents have perfect recall. Studies have thus mostly focused either on agents without memory, or on alternative semantics to retrieve decidability. In this work we establish new decidability results for agents with perfect recall: We first prove a meta-Theorem that allows the transfer of decidability results for classes of multiplayer games with imperfect information, such as games with hierarchical observation, to the model-checking problem for ATL J. We then establish that model checking ATL∗ with strategy context and imperfect information is decidable when restricted to hierarchical instances.
Decidability results for ATL∗ with imperfect information and perfect recall / Berthon, R.; Maubert, B.; Murano, A.. - 2:(2017), pp. 1250-1258. (Intervento presentato al convegno 16th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2017 nel 2017).
Decidability results for ATL∗ with imperfect information and perfect recall
Maubert B.;Murano A.
2017
Abstract
Alternating-Time Temporal Logic (ATL∗) is a central logic for multiagent systems. Its extension to the imperfect information setting (ATLJ) is well known to have an undecidable model-checking problem when agents have perfect recall. Studies have thus mostly focused either on agents without memory, or on alternative semantics to retrieve decidability. In this work we establish new decidability results for agents with perfect recall: We first prove a meta-Theorem that allows the transfer of decidability results for classes of multiplayer games with imperfect information, such as games with hierarchical observation, to the model-checking problem for ATL J. We then establish that model checking ATL∗ with strategy context and imperfect information is decidable when restricted to hierarchical instances.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.