This short introductory chapter starts by recalling how the alternating-time temporal logics have been introduced by Rajeev Alur, Thomas Henzinger and Orna Kupferman about twenty-five years ago. Such logics extend the branching-time temporal logics used in the model-checking approach for formal verification of programs and are dedicated to open systems. The chapter also illustrates how active is the current research on alternating-time temporal logics that is at the crossroads of several topics, including model-checking, logics for strategic reasoning and games. The second part of the chapter presents the general organization of the document as well as the motivations for focusing on the model-checking problem. Typically, it is deliberate that only elementary material about alternating-time temporal logics is provided. In particular, the technical developments are designed so that the meta-reasoning about strategies can be done smoothly but with enough mathematical details. The document mainly contains standard results voluntarily exposed in a pedestrian style, and a few more recent results that are developed in full depth in order to prepare the reader to investigate more elaborate logical formalisms.