Séminaires
Séminaire du 7 février 2014
Lieu
LACL, salle des thèse : comment y aller
Programme
14h00-15h00: Mathieu Sassolas, LACL, "Jeux pour la vérification et la synthèse: le cas de l'admissibilité pour des objectifs oméga-réguliers"
Abstract: 
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).
L'élimination des stratégies consiste à éliminer les stratégies qui fournissent toujours de moins bons résultats (vis-à-vis de l'objectif du joueur) qu'une autre.
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.
15h00-15h30 : Etienne Renault, LIP6 & LRDE, "trois tests de vacuité basés dur les SCC pour les automates de Büchi généralisés"
Abstract: L’approche automate pour la vérification de logique temporelle linéaire implique de tester la vacuité (emptiness check) d’un automate de Büchi. Cependant les automates de Büchi généralisés, avec plusieurs ensembles d’acceptations, sont préférés lors de la vérifications sous des hypothèses d’équité. Des algorithmes d’emptiness check dont la complexité est indépendante du nombre de conditions d’acceptations existent et sont tous basés sur l’énumération des composantes fortement connexes (CFC).
Cette présentation présente les algorithmes classiques d’énumération des composantes fortement connexes et montre comment ils peuvent être transformés en test de vaccuité généralisé. Pour cela deux nouveaux algorithmes seront introduits (un d’entre eux basé sur un Union-Find) ainsi que de nouvelles optimisations qui peut être appliqué dans des algorithmes de calcul de CFC.
La comparaison des différents algorithmes sera présentés ainsi que le surcout par rapport aux algorithmes de calcul de CFC.