Jeux discrets pour la synthèse et la validation de processus communicants

L'étude des jeux discrets infinis occupe une place importante au sein des travaux sur la vérification et la synthèse automatique de programmes. Les jeux à deux joueurs fournissent un formalisme simple pour l'étude des systèmes ouverts, où un système informatique interagit avec son environnement. Dans le contexte de la synthèse de programmes distribués, les jeux à deux joueurs ne suffisent plus : on doit disposer d'un modèle de jeux où un nombre arbitraire de joueurs coopèrent. Dans cette thèse, je m'ntéresse à deux modèles de jeux pour la synthèse de programmes. J'étudie dans un premier temps les jeux de parité, en proposant une notion de stratégie permissive, qui capture le fait qu'un programme accepte un nombre de comportements au moins aussi grand que tous les programmes corrects. Je propose en outre un algorithme efficace pour le calcul des stratégies permissives dans un jeu de parité. Dans un deuxième temps, je m'intéresse aux jeux distribués, où une équipe de joueurs Processus affronte un joueur Environnement, en disposant de communications incomplètes entre eux. Je montre que le problème de la synthèse d'une stratégie gagnante dans ces jeux est indécidable, même dans le cas de conditions de gain très simples. Je m'attache alors à définir une classe de jeu distribués au sein de laquelle le problème de la synthèse est décidable, et je montre quelles conséquences en découlent pour un problèmes de synthèse de programmes distribuée classique.BORDEAUX1-BU Sciences-Talence (335222101) / SudocSudocFranceF