The alternating-time temporal logic ATL complements the more classical logics LTL and CTL with a way of expressing properties of open systems, interacting with external, uncontrollable components. ATL was introduced 15 years ago, and is now rather well understood. While it enjoys efficient model-checking algorithms, ATL is quite limited in terms of expressiveness: it can only express zero-sum objectives, and thus mainly focuses on purely antagonistic two-player games. Several recent extensions of ATL have been proposed in order to express properties of non-zero-sum games, mixing antagonism and collaboration. After introducing the classical logics, this course will explore those extensions in terms of their expressiveness and algorithms, using a tigh link with the extension of CTL with quantification over atomic propositions.