I will introduce and discuss some of the most important and popular families of logics for multi-agent systems: epistemic, dynamic epistemic (unless covered in another ESSLLI course), temporal-epistemic, and logics of strategic abilities of the type of ATL. Eventually, I will introduce a general logical framework for modeling of knowledge, communication, actions and strategic abilities of agents and coalitions in MAS, and analyzing the dynamics of interaction of these. At the end of the course I will discuss possible applications of that framework to verification and synthesis of communication and security protocols.
The emphasis of the course will be on understanding of the languages and semantics of these logics, and on applying them to model and specify properties of MAS. I illustrate these with several well-known scenarios and problems. The main logical decision problems, such as model checking and validity/satisfiability testing, will be introduced but not discussed in details, and technical results for these will only be mentioned.
