November 18, 2013
Mathieu Sassolas (LACL - UPEC)Les jeux ont pris une place croissante dans le domaine de la vérification formelle de systèmes, en particulier parce qu’ils permettent également la synthèse de contrôleurs pour le système. Plusieurs notions qui avaient tout d’abord été proposées dans le cadre de modélisation de systèmes économiques ont été adaptées au contexte des jeux sur des graphes: dans le cas de jeux multijoueurs, on retient le plus souvent le concept d’équilibre de Nash. Mais d’autres paradigmes ont également été adaptés, en particulier celui d’élimination de stratégies dominées, qui est celui qui retiendra notre attention dans cet exposé.
Après avoir fait un bref tour d’horizon des applications des jeux pour la vérification, je m’intéresserai plus précisément à l’élimination itérative de stratégies dominées dans des jeux multijoueurs (infinis) sur des graphes (finis). Ici, chaque joueur dispose d’un objectif oméga-régulier qui n’est pas nécessairement en opposition avec celui des autres joueurs (jeu dit à somme non nulle). Dans ce cadre nous étudions l’algorithmique de problèmes naturels à propos de l’ensemble des stratégies admissibles – celles survivant toutes les phases d’élimination–, et obtenons leur complexité exacte. De plus, nous obtenons un automate reconnaissant l’ensemble des exécutions possibles lorsque tous les joueurs choisissent une stratégie admissible.
Les résultats présentés sont issu d’un travail conjoint avec Romain Brenguier et Jean-François Raskin.