Valentin Goranko: Logical modelling, specification, verification and synthesis of multi-agent systems: an introduction

Abstract
In this talk I will introduce concurrent game models for multi-agent systems and the Alternating-time temporal logic ATL as the currently most popular logical system for formalizing and reasoning about strategic abilities in such systems.
I will illustrate the semantics of ATL with some examples and will discuss briefly the logical decision problems of model checking and constructive satisfiability testing of ATL formulae, and how these can be used for specification, verification, and synthesis of concurrent game models.