[1] ATL naturally describes computations of multi-agent systems and concurrent games.
[3] ATL uses alternating-time formulas to construct model-checkers in order to address problems such as receptiveness, realizability, and controllability.
Belardinelli et al. proposes a variant of ATL on finite traces.
[4] ATL has been extended with context, in order to store the current strategies played by the agents.
[5] In 2004, Pierre-Yves Schobbens proposed variants of ATL with imperfect recall.