Formal logic is widely regarded as a foundation for specification, verification and reasoning about multi-agent systems. In recent years, a new group of modal logics emerged. These logics focus on the notion of strategy, and try to address abilities of agents in environments that involve many autonomous entities acting in parallel.
In this course, we present an overview of results and algorithms for decision problems in propositional strategic logics, with a special focus on Alternating-time Temporal Logic (ATL). We begin with an introduction of basic concepts and logics, then we present existing results for the satisfiability/validity problem; finally, we discuss model checking and show how its complexity changes when we change the way the details of the problem are defined. The rest of the course is devoted to more sophisticated models of agent behavior, including rationality assumptions, bounded resources, and imperfect information scenarios.