Soutenance de thèse - Julien Reichert

Titre

Décidabilité et complexité de jeux d'accessibilité sur des systèmes à compteurs

Informations pratiques

Quand ?Le jeudi 30 juillet 2015 à 10 h
Où ?À la salle de conférences du Pavillon des Jardins, sur le campus de l'ENS Cachan

Jury

Le jury se compose de :

Résumé

Dans cette thèse, nous considérons le problème consistant à déterminer le vainqueur de différents modèles de jeux d'accessibilité sur des systèmes à compteurs. Un jeu sur un graphe est joué par deux joueurs à qui les états du système appartiennent. Au cours d'une partie, les joueurs construisent une exécution du système en déplaçant un jeton d'état en état le long des transitions, le choix de chaque transition étant laissé au joueur à qui appartient l'état où le jeton se trouve. Les transitions mettent à jour un vecteur de compteurs, généralement par l'addition d'un vecteur. Les configurations des systèmes à compteurs sont des paires composées d'un état du système et d'un vecteur formé par les valeurs des compteurs. Dans les jeux d'accessibilité sur des systèmes à compteurs, l'objectif du premier joueur est d'atteindre une configuration particulière. Le problème de décision associé à un jeu d'accessibilité consiste à déterminer si le premier joueur a une stratégie gagnante dans le jeu depuis une configuration initiale donnée.

L'essentiel de notre étude suit deux directions : d'une part, nous comparons des modèles dont la différence réside dans la sémantique, d'autre part nous considérons un modèle sans états de systèmes à compteurs. Concernant la première direction, la sémantique dépend du comportement du système quand un compteur devrait devenir négatif. Nous nous focalisons principalement sur trois sémantiques, dont le modèle standard des systèmes d'additions de vecteurs avec états. Concernant la seconde direction, nous étudions un modèle intitulé « robot games », où il n'y a qu'un état pour chaque joueur, sans boucle sur les états.

Nos résultats principaux concernant les sémantiques des systèmes sont des réductions mutuelles entre les problèmes de décision avec les trois sémantiques principales. Nos résultats principaux sur le modèle des robot games sont les suivants. En dimension une, nous décrivons un algorithme de complexité optimale et moindre que la complexité de la détermination du vainqueur de jeux d'accessibilité sur des systèmes à compteurs. Nous prouvons également que les robot games sont indécidables en dimension trois, et la décidabilité en dimension deux demeure une question ouverte.

Manuscrit

La dernière version du manuscrit est disponible ici.

À propos du LSV