2- Course Aim :

Multi agent systems (MAS) course provides an important framework for formalizing various problems in computer science, artificial intelligence, game theory, social choice theory, etc. Modal logics are amongst the most suitable and versatile logical formalisms for specification and verification of computational systems. The course offers an introduction to some important developments in the area. We introduce modal logics used for specification of temporal, epistemic, and strategic properties of systems; then, we present model checking algorithms based on Binary Decision Diagrams (BDD) and satisfiability solving (SAT), and discuss the computational complexity of the model checking problem. We also consider symbolic (compact) representations of systems, and how the representations change the semantic and algorithmic side of model checking. Finally, we discuss some techniques that help to reduce the complexity and make verification feasible even for large systems.