Stéphane Demri, CNRS researcher at LMF, has published Concise Introduction to Alternating-Time Temporal Logics: A Guide for Understanding the Model-Checking Problem.
From the publisher’s description: This textbook provides a concise presentation of alternating-time temporal logics dedicated to strategic reasoning in multi-agent systems. Dedicated mainly to the model-checking problem, the work examines developments about basic semantical properties of such logics, decision procedures and computational complexity. It provides results for solving optimally the model-checking problem on concurrent game structures by taking advantage of—or adapting proof methods from—temporal logics, games in theoretical computer science and automata theory.More information is available on the publisher’s page.