# Decidability results for ATL* with imperfect information and perfect recall

arXiv: https://arxiv.org/abs/1805.12582 · HTML: https://mlsanity.com/paper/1805.12582/

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 31 May 2018.

## Built on by (most cited first, 5 of 5)

- [On Alternating-Time Temporal Logic, Hyperproperties, and Strategy Sharing](https://mlsanity.com/paper/2312.12403/) (2023)
- [Hyper Strategy Logic](https://mlsanity.com/paper/2403.13741/) (2024)
- [Model Checking Strategic Abilities in Information-sharing Systems](https://mlsanity.com/paper/2204.08896/) (2022)
- [Strategy Logic, Imperfect Information, and Hyperproperties](https://mlsanity.com/paper/2510.03952/) (2025)
- [A Neuro-Symbolic Approach to Strategy Synthesis for Strategic Logics](https://mlsanity.com/paper/2606.17962/) (2026)

## Abstract (arXiv)

Alternating-time Temporal Logic (ATL*) is a central logic for multiagent systems. Its extension to the imperfect information setting (ATL*i ) 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*i . We then establish that model checking ATL* with strategy context and imperfect information is decidable when restricted to hierarchical instances.