Jeux et Automates, Décidabilité et Extensions – JADE

La théorie des automates a vu le jour il y a une cinquantaine d'années avec les travaux fondateurs de Kleene. Si la première motivation était l'étude des réseaux neuronaux, son champ d'application s'est largement diversifié et s'étend aujourd'hui de la linguistique à la théorie du contrôle en passant par la biologie, la compression de données, l'analyse de système et bien d'autres encore. Dès lors de nombreuses variantes de cette théorie ont été développées et des connexions avec des théories mathématiques profondes (comme la logique, l'algèbre, ou la topologie) sont apparues. C'est dans cette perspective que se place ce projet où nous considérerons différentes variantes des automates, avec un intérêt particulier pour la théorie des automates finis sur des objets infinis, tels que les arbres. Dans ce dernier cas, les automates possèdent un nombre fini d'états, une fonction de transition classique et sont équipés d'annotations particulières permettant de définir la notion d'exécution acceptante, même quand celle-ci est infinie. Le résultat fondateur de Rabin énonce que les automates d'arbre infinis dits de Rabin, forment une algèbre de Boole. - - La théorie des jeux est également un sujet très vaste: économie, mathématiques, informatique sont ses grands domaines d'application. En informatique, un jeu voit deux joueurs antagonistes s'affronter au cours d'une partie où ils jouent à tour de rôle, et ce pendant une durée éventuellement infinie. Déterminer le vainqueur est alors le principal problème algorithmique qui se pose. Les jeux se révèlent être un outil de preuve puissant, car ils permettent de modéliser de nombreux problèmes de décision: une première étape consiste à traduire le problème en un jeu équivalent et ensuite de résoudre le jeu. C'est dans ce dernier point que se situe souvent la difficulté et que l'emploi du concept de stratégie est précieux. La notion de stratégie, qui en général n'a que peu de sens sur le problème original s'étudie alors comme un objet mathématique à part entière. En particulier, on montre que si le premier joueur gagne, alors il peut gagner en utilisant une stratégie d'une certaine forme particulière: le nombre de stratégies s'en trouve alors drastiquement réduit, et quand une infinité non-dénombrable de stratégies étaient envisageables à priori, seul un nombre fini ont la forme souhaitée. Une recherche exhaustive permet alors de conclure. Ce cadre général est en particulier au coeur de toutes les preuves modernes du théorème de Rabin. - - Plusieurs problèmes nous semblent tout particulièrement intéressants. - - Automates d'arbre infinis avec des contraintes d'égalités entre les sous-arbres. On autorise, dans la fonction de transition, des tests d'égalité ou d'inégalité entre les sous-arbres du noeud courant. Si dans le cas des arbres finis le test du vide est décidable, le problème est plus délicat dans le cas des arbres infinis. Il convient de comprendre d'où vient cette difficulté et comment la résoudre. - - Extensions décidables de la théorie monadique du second ordre (MSO). De récents travaux montrent que, contrairement à l'idée communément admise, il est possible de résoudre des logiques plus expressives que la logique MSO. Ces travaux offrent de nombreuses perspectives en vérification, et entraînent la définition de familles plus générales d'automates aux propriétés nouvelles. Leur étude, ainsi que celle des jeux associés est un important sujet que les membresdu projet comptent développer. - - Jeux positionellement déterminés. Les stratégies les plus simples sont celles qui ne nécessitent pas de mémoire (dites positionnelles). L'existence d'une telle stratégie dépend à la fois de la condition de gain et de la structure du graphe de jeu. L'objectif est, pour une famille de graphes de jeu fixée (e.g. graphes finis ou graphes infinis bien particuliers) de caractériser les conditions de gain pour lesquelles il existe toujours une stratégie gagnante positionnelle. Ce problème n'est c