Temporal logics for multi-player games

Nicolas Markey
LSV / CNRS & ENS Cachan
Friday, 29 January, 2016 - 14:00
P.2NO9.06 (La Plaine)

The alternating-time temporal logic (ATL) was defined 15 years ago as an extension of CTL for expressing and verifying properties of multi-player games. However, in order to inherit nice algorithmic properties of CTL, ATL has limited expressiveness: it cannot really express strategic interactions between several players. In this talk, I will present our extension of ATL with strategy contexts, which contrary to ATL can express rich properties with interactions between strategies (e.g. equilibria properties). I will then present our results about model checking and satisfiability for this logic, using quantified CTL as an intermediary tool. This talk is based on joint works with Thomas Brihaye, Arnaud Da Costa Lopes, and François Laroussinie.