Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
Concept
Automate de Büchi
Résumé
En informatique théorique, un automate de Büchi est un ω-automate ou automate fini opérant sur des mots infinis, avec une condition d'acceptation particulière : une trace (ou calcul ou chemin infini) est réussie si et seulement si elle passe un nombre infini de fois par au moins un état acceptant. Un mot infini est accepté s'il est l'étiquette d'un calcul réussi. Ce type d'automate est utilisé en vérification de modèles.
Ce type d'automate a été défini par le mathématicien Julius Richard Büchi.
Un automate de Büchi sur un alphabet est un ω-automate , où :
est un ensemble fini détats ;
est l'ensemble des transitions ;
est l'ensemble des états initiaux ;
est un ensemble d'états finals ou terminaux ou acceptants.
Souvent on suppose que l'ensemble des états initiaux est composé d'un seul élément.
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 . Le calcul est réussi et le mot est accepté ou reconnu s'il passe infiniment souvent par un état terminal.
Un automate est déterministe s'il vérifie les deux conditions suivantes :
il possède un seul état initial ;
pour tout état , et pour toute lettre , il existe au plus une transition partant de et portant l'étiquette .
L'automate de Büchi déterministe donné par , avec
deux états : et . L'état est initial. L'ensemble des états acceptants est .
La fonction de transition est montrée dans le dessin à gauche.
Le mot infini n'est pas accepté car la seule trace correspondante est et le seul état qui apparaît une infinité de fois est qui ne figure pas dans . Par contre, le mot est accepté car il possède la trace , et y apparaît une infinité de fois et est dans . Il reconnaît les mots infinis contenant un nombre infini de . En rencontrant la lettre , l'automate retourne dans l'état , alors qu'une lecture de la lettre met l'automate dans l'état .
Source officielle
À 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.