Temporal logics for multi-agent systems: expressiveness and algorithms

Topic: 
Logic & Computation
Level: 
Introductory
Abstract: 

The alternating-time temporal logic ATL complements the more classical logics LTL and CTL with a way of expressing properties of open systems, interacting with external, uncontrollable components. ATL was introduced 15 years ago, and is now rather well understood. While it enjoys efficient model-checking algorithms, ATL is quite limited in terms of expressiveness: it can only express zero-sum objectives, and thus mainly focuses on purely antagonistic two-player games. Several recent extensions of ATL have been proposed in order to express properties of non-zero-sum games, mixing antagonism and collaboration. After introducing the classical logics, this course will explore those extensions in terms of their expressiveness and algorithms, using a tigh link with the extension of CTL with quantification over atomic propositions.

Week: 
Second week
Slot: 
17:00 - 18:30 - slot 4
Room: 
52.117