The first part of the chapter is dedicated to the proof establishing that the model-checking problem for ATL+ is PSPACE-complete. The PSPACE-hardness is by reduction from the PSPACE-complete problem QBF. The PSPACE-membership is established by showing that winning strategies can be characterized by strategy skeletons that summarize the strategies, so that such finite structures can be guessed using polynomial-space only. Furthermore, we show that the core model-checking problem for ATL+ can be reduced to solving Büchi games, which allows us to establish that the problem is in PTIME when some specific syntactic resources in path formulae are bounded. The correspondence between the core model-checking problem and two-player game problems is natural and often evoked in the literature. We reduce the core model-checking problem for ATL* to solving parity games, by making use of the determinization of Büchi automata by parity automata. There is a double exponential blow-up but this allows us to conclude that the core model-checking problem for ATL* is in 2EXPTIME, whence we get the same complexity upper bound for the model-checking problem for ATL*. The chapter concludes by considering the variant of ATL-like logics in which quantifications over strategies are restricted to positional ones. We show that the model-checking problem for ATL* restricted to positional strategies is PSPACE-complete as well as for a variant of ATL in which the satisfaction relation carries a strategy context and the strategies are memoryless.