 Another important family of temporal logics of agency are the alternating-time logics ATL and ATL*, introduced in Alur et al. (2002). ATL and ATL* are multi-agent extensions of the computation tree logics CTL and CTL*, and they have become a popular logical framework for strategic reasoning in multi-agent systems. Alternating-time temporal logics enrich the language with strategic path quantifiers \(\langle\!\langle C \rangle\!\rangle \varphi,\) intuitively saying “The coalition \(C\) has a collective strategy to guarantee that the objective \(\varphi\) is met on every path enabled by that collective strategy”, where the objective \(\varphi\) is a temporal formula. While stit logics build on the rather abstract notion of a history, ATL and ATL* are interpreted over so-called concurrent game structures, in which paths are viewed as sequences of successor states that are generated by discrete transitions caused by collective actions of all agents. A combination of ATL and stit theory was developed in Broersen et al. (2006). The branching time logics CTL and CTL* can be regarded as single-agent versions of ATL and ATL*. Even though the latter are quite more expressive, they generally preserve the good computational properties of the former. For further details, see Alur et al. (2002), as well as Goranko and van Drimmelen (2006), where a complete axiomatization and decidability results for ATL are established. A general introduction to ATL from a temporal logic perspective is provided in Demri et al. (2016, Chapter 9).