Concept

Automate sur les mots infinis

Résumé
En informatique théorique, et spécialement en théorie des automates, un automate sur les mots infinis ou ω-automate est un automate fini qui accepte des mots infinis. Un tel automate lit un mot infini, ainsi, l'exécution ne s'arrête pas ; les conditions d'acceptation portent sur l'exécution elle-même là où elles ne traitent que de l'état d'arrivée (et de la possibilité de lire le mot) dans le cas des automates sur les mots finis. Les automates sur les mots infinis servent à modéliser des calculs qui ne terminent pas, comme le comportement d'un système d'exploitation, ou d'un système de contrôle. Pour de tels systèmes, on peut spécifier des propriétés comme « chaque requête sera suivie d'une réponse » ou sa négation « il existe une requête qui n'est pas suivie d'une réponse ». De telle propriétés peuvent être formulées pour des mots infinis et peuvent être vérifiées par des automates finis. Plusieurs classes d'automates sur les mots infinis ont été introduites : les automates de Büchi, automates de Rabin, automates de Streett, automates de parité, automates de Muller et, pour chaque classe, les automates déterministes ou non. Ces classes diffèrent seulement par leur condition d'acceptation. Toutes ces classes, à l'exception notable des automates de Büchi déterministes, reconnaissent la même famille d'ensembles de mots infinis, appelés ensembles rationnels de mots infinis ou ω-langages rationnels. Ces automates, même s'ils acceptent les mêmes langages, peuvent varier en taille pour un langage donné. Comme pour les automates finis, un automate sur les mots infinis sur un alphabet est un quadruplet , où : est un ensemble fini d'états, est l'ensemble des transitions, est l'ensemble des états initiaux, et est un ensemble d'états finals ou terminaux. Souvent on suppose qu'il existe un seul état initial. Une transition est composée d'un état de départ , d'une étiquette et d'un état d'arrivée . Un 'calcul (on dit aussi un chemin' ou une trace) est une suite infinie de transitions consécutives : Son état de départ est , son étiquette est le mot infini .
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.