Previous Up Next

Automates sur mots infinis

Cours de recherche (30h de cours, travail sur des articles scientifiques)

Cours : Olivier Finkel (Olivier.Finkel)

Les automates sur mots infinis ont été introduits par Büchi dans les années 1960 pour étudier la décidabilité de la théorie d'un successeur sur les entiers. Ils ont depuis été très étudiés et utilisés pour la spécification et la vérification de systèmes ne terminant pas, comme un système d'exploitation.

La théorie des automates lisant des mots infinis a des liens avec de nombreux domaines, en particulier avec la topologie, la logique, les jeux infinis qui modélisent le comportement d'un système en interaction avec un environnement.

On présentera les notions classiques d'acceptation de mots infinis par automates finis et on étudiera les aspects fondamentaux de cette théorie. On abordera l'étude des jeux infinis, modélisant le comportement d'un système en interaction avec un environnement, et la construction de stratégies gagnantes effectives dans ces jeux. Cette construction correspond à la synthèse de programmes dans les systèmes réactifs.

En fonction du temps, plusieurs extensions seront considérées, comme :
Bibliographie

Previous Up Next