Concurrent game structures understood as multi-agent extensions of transition systems are introduced in the chapter, as well as the related notions of histories, computations and strategies. The alternating-time temporal logic ATL is then defined using concurrent game structures as models and the logical connectives include strategy modalities, that correspond to existential quantifications over strategies for the proponent coalitions. The semantics for the strategy modalities in ATL is captured by fixpoint characterizations, in the same way the temporal connectives in the branching-time logic CTL can be characterized by fixpoints. We provide such characterizations and show its correctness, which will be instrumental to design the labelling algorithm to decide the model-checking problem for ATL. Generalizing the class of objectives, we present the extensions ATL+ and ATL* by enriching the class of path formulae. We also show that the branching-time temporal logics CTL, CTL+ and CTL* are respectively fragments of ATL, ATL+ and ATL*. The chapter concludes by presenting the issues related to imperfect information and how it is encoded in concurrent game structures by adding indistinguishability relations parameterized by agents. New logics are defined, such as ATL with imperfect information and memoryful strategies.