9 novembre 2015
Nicolas Markey (LSV, ENS Cachan)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. In this talk, I will begin with presenting our extension of ATL with strategy contexts, which contrary to ATL can express rich properties with interactions between strategies. I will then present QCTL, the extension of CTL with quantification over atomic propositions, and explain how it can be used to get algorithms for ATL with strategy contexts. This talk is based on joint works with Thomas Brihaye, Arnaud Da Costa Lopes, and François Laroussinie.