Automate de Büchi

Un automate de Büchi sur un alphabet ${\displaystyle A}$ est un ω-automate ${\displaystyle {\mathcal {A}}=(Q,{\mathcal {F}},I,T)}$, où :

• ${\displaystyle Q}$ est un ensemble fini d'états ;
• ${\displaystyle {\mathcal {F}}\subset Q\times A\times Q}$ est l'ensemble des transitions ;
• ${\displaystyle I\subseteq Q}$ est l'ensemble des états initiaux ;
• ${\displaystyle T\subseteq Q}$ 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[2]. Une transition ${\displaystyle f=(p,a,q)}$ est composée d'un état de départ ${\displaystyle p}$, d'une étiquette ${\displaystyle a}$ et d'un état d'arrivée ${\displaystyle q}$. Un calcul ${\displaystyle c}$ (on dit aussi un chemin ou une trace) est une suite infinie de transitions consécutives :

${\displaystyle c=(p_{0},a_{1},p_{1})(p_{1},a_{2},p_{2})\cdots }$

Son état de départ est ${\displaystyle p_{0}}$, son étiquette est le mot infini ${\displaystyle a_{1}a_{2}\cdots a_{n}\cdots }$. 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 ${\displaystyle q}$, et pour toute lettre ${\displaystyle a}$, il existe au plus une transition partant de ${\displaystyle q}$ et portant l'étiquette ${\displaystyle a}$.

Automate de Büchi ${\displaystyle {\mathcal {A}}}$ reconnaissant les mots infinis contenant un nombre infini de ${\displaystyle a}$.

L'automate de Büchi déterministe donné par ${\displaystyle {\mathcal {A}}=(\{q_{0},q_{1}\},{\mathcal {F}},q_{0},\{q_{1}\})}$, avec deux états : ${\displaystyle q_{0}}$ et ${\displaystyle q_{1}}$. L'état ${\displaystyle q_{0}}$ est initial. L'ensemble des états acceptants est ${\displaystyle T=\{q_{1}\}}$. La fonction de transition ${\displaystyle {\mathcal {F}}}$ est montrée dans le dessin à gauche.

Le mot infini ${\displaystyle bbbb\cdots }$ n'est pas accepté car la seule trace correspondante est ${\displaystyle q_{0}q_{0}q_{0}\cdots }$ et le seul état qui apparaît une infinité de fois est ${\displaystyle q_{0}}$ qui ne figure pas dans ${\displaystyle T}$. Par contre, le mot ${\displaystyle aaaa\cdots }$ est accepté car il possède la trace ${\displaystyle q_{0}q_{1}q_{1}\cdots }$, et ${\displaystyle q_{1}}$ y apparaît une infinité de fois et est dans ${\displaystyle T}$. Il reconnaît les mots infinis contenant un nombre infini de ${\displaystyle a}$. En rencontrant la lettre ${\displaystyle b}$, l'automate retourne dans l'état ${\displaystyle q_{0}}$, alors qu'une lecture de la lettre ${\displaystyle a}$ met l'automate dans l'état ${\displaystyle q_{1}}$. Plus généralement, l'automate accepte exactement les mots infinis sur deux lettres ${\displaystyle a}$ et ${\displaystyle b}$ qui ne contiennent qu'un nombre fini de lettres ${\displaystyle a}$, c'est-à-dire l'ensemble ${\displaystyle b^{*}a(a^{*}b^{+}a)^{\omega }}$.

Automate de Büchi reconnaissant les mots infinis où chaque occurrence de ${\displaystyle b}$ est précédé d'un nombre pair non nul de ${\displaystyle a}$.

Un autre exemple est l'automate de Büchi à droite ; il reconnaît les mots infinis où chaque occurrence de ${\displaystyle b}$ est précédé d'un nombre pair non nul de ${\displaystyle a}$. L'automate possède trois états : ${\displaystyle q_{0}}$, ${\displaystyle q_{1}}$ et ${\displaystyle q_{2}}$. Il est aussi déterministe. L'automate démarre dans l'état ${\displaystyle q_{0}}$ et lit un nombre pair non nul de ${\displaystyle a}$. Si l'automate a lu un nombre impair de ${\displaystyle a}$, il est dans l'état ${\displaystyle q_{1}}$, sinon dans l'état ${\displaystyle q_{2}}$. La transition ${\displaystyle b}$ de l'état ${\displaystyle q_{2}}$ à l'état ${\displaystyle q_{0}}$ permet de lire la lettre ${\displaystyle b}$ après un nombre pair non nul de ${\displaystyle a}$. Une lecture de ${\displaystyle b}$ depuis ${\displaystyle q_{0}}$ ou ${\displaystyle q_{1}}$ échoue.

Les automates de Büchi déterministes sont strictement moins puissants que les automates de Büchi non déterministes[3] - [4]. Par exemple, alors qu'il existe un automate de Büchi non déterministe à deux états qui reconnaît les mots infinis sur deux lettres ${\displaystyle a}$ et ${\displaystyle b}$ qui ne contiennent qu'un nombre fini de lettres ${\displaystyle a}$, c'est-à-dire l'ensemble ${\displaystyle \{a,b\}^{*}b^{\omega }}$, cet ensemble n'est pas reconnu par un automate de Büchi déterministe.

Supposons le contraire, c'est-à-dire qu'il existe un automate de Büchi déterministe qui reconnaît ce langage, et soit ${\displaystyle F}$ son ensemble d'états d'acceptation. L'automate accepte le mot infini ${\displaystyle b^{\omega }}$, dont le calcul passe une première fois dans un état de ${\displaystyle F}$ après la lecture d'un certain nombre positif, disons ${\displaystyle n}$, de lettres ${\displaystyle b}$. L'automate accepte aussi le mot infini ${\displaystyle b^{n}ab^{\omega }}$, donc le calcul passe une deuxième fois par un état de ${\displaystyle F}$ après disons ${\displaystyle m}$ lettres ${\displaystyle b}$. L'automate accepte donc le mot ${\displaystyle b^{n}ab^{m}ab^{\omega }}$. De proche en proche, on construit un mot ${\displaystyle b^{n_{1}}ab^{n_{2}}ab^{n_{3}}ab\cdots }$ contenant une infinité de lettres ${\displaystyle a}$ et qui est accepté par l’automate, contradiction.

Les ensembles de mots infinis reconnus par les automates de Büchi sont les ensembles rationnels de mots infinis ou ω-langages rationnels, à savoir les ensembles de la forme

${\displaystyle \bigcup _{1}^{m}U_{i}V_{i}^{\omega }}$

où les ${\displaystyle U_{i}}$ et ${\displaystyle V_{i}}$ sont des langages rationnels pour tout ${\displaystyle i}$, les ${\displaystyle V_{i}}$ ne contenant pas le mot vide. Ces langages sont aussi appelés les ω-fermeture de Kleene des langages rationnels[5].

La formule pour l'expression du langage reconnu par un automate de Büchi s'obtient comme suit : étant donné une automate de Büchi, notons ${\displaystyle W(p,q)}$ l’ensemble des mots finis reconnus avec ${\displaystyle p}$ comme état initial et ${\displaystyle q}$ comme état final, donc les mots qui sont étiquettes d’un chemin de ${\displaystyle p}$ à ${\displaystyle q}$. Ces langages (de mots finis) sont rationnels. Un mot infini ${\displaystyle x}$ est accepté s’il existe un calcul qui passe une infinité de fois par un état final, donc aussi s’il existe un état final disons ${\displaystyle q}$, par lequel il passe une infinité de fois. Ceci est équivalent à dire que

${\displaystyle x\in W(q_{0},q)W(q,q)^{\omega }}$

pour un état initial ${\displaystyle q_{0}}$. En prenant la réunion sur tous les états initiaux et terminaux, on obtient la description indiquée[5]. Pour démontrer que réciproquement tous les ω-langages rationnels sont reconnus par des automates de Büchi, on utilise les opérations de fermeture de la section suivante[6].

La description effective des ω-langages rationnels reconnus montre que le problème du mot est décidable pour les automates de Büchi, puisqu’il suffit de tester si l’un au moins des langages rationnels ${\displaystyle W(q_{0},q)W(q,q)}$ n’est pas vide.

Les langages reconnus par des automates de Büchi fermés pour un certain nombre d'opérations qui se reflètent dans des constructions sur les automates.

• Union : Soient ${\displaystyle {\mathcal {A}}=(Q_{A},{\mathcal {F}}_{A},I_{A},T_{A})}$ et ${\displaystyle {\mathcal {B}}=(Q_{B},{\mathcal {F}}_{B},I_{B},T_{B})}$ reconnaissant respectivement les langages ${\displaystyle L_{A}}$ et ${\displaystyle L_{B}}$. Un automate reconnaissant la réunion ${\displaystyle L_{A}\cup L_{B}}$ s'obtient en faisant la réunion des deux automates. On suppose les ensembles d'états de ${\displaystyle {\mathcal {A}}}$ et ${\displaystyle {\mathcal {B}}}$ disjoints ; alors l’automate ${\displaystyle {\mathcal {C}}=(Q_{A}\cup Q_{B},{\mathcal {F}}_{A}\cup {\mathcal {F}}_{B},I_{A}\cup I_{B},T_{A}\cup T_{B})}$ reconnaît la réunion.

• ω-fermeture : Pour tout langage rationnel ${\displaystyle L}$ ne contenant pas le mot vide, le ω-langage ${\displaystyle L^{\omega }}$ est reconnu par un automate de Büchi. Soit ${\displaystyle {\mathcal {A}}=(Q,{\mathcal {F}},i,T)}$ un automate fini reconnaissant ${\displaystyle L}$. On peut supposer qu'il n'a qu'un seul état initial noté ${\displaystyle i}$, et qu'il n'y a pas de transition entrant dans ${\displaystyle i}$. On ajoute à l'automate ${\displaystyle {\mathcal {A}}}$ les transitions ${\displaystyle (q,a,i)}$ pour chaque transition ${\displaystyle (q,a,t)}$ de \mathcal{F} avec ${\displaystyle t\in T}$. L'automate de Büchi ainsi construit, avec un seul état initial qui est aussi terminal, reconnaît ${\displaystyle L^{\omega }}$.

• Concaténation : Pour tout langage rationnel ${\displaystyle L}$ et tout ω-langage ${\displaystyle M}$ reconnu par un automate de Büchi, le produit ${\displaystyle LM}$ est un ω-langage reconnu par un automate de Büchi. Soient en effet ${\displaystyle {\mathcal {A}}=(Q,{\mathcal {F}},i,T)}$ un automate fini reconnaissant ${\displaystyle L}$, avec ${\displaystyle I\cap T=\emptyset }$, et ${\displaystyle {\mathcal {B}}=(Q',{\mathcal {F'}},I',T')}$ un automate de Büchi reconnaissant ${\displaystyle M}$. On peut supposer les ensembles d'états des deux automates disjoints. On peut aussi supposer que ${\displaystyle L}$ ne contient pas le mot vide, sinon on remplace le produit ${\displaystyle LM}$ par ${\displaystyle (L\setminus \varepsilon )M\cup M}$. On construit un automate de Büchi ${\displaystyle {\mathcal {C}}}$ qui a pour états l'union des ensembles d'états, pour transitions l'union des ensembles de transitions, augmentées des transitions ${\displaystyle (q,a,i')}$ pour ${\displaystyle i'\in I'}$ pour chaque transition ${\displaystyle (q,a,t)}$ de ${\displaystyle {\mathcal {F}}}$ qui mène vers un état terminal ${\displaystyle t}$ de ${\displaystyle {\mathcal {A}}}$. Enfin, ses états initiaux sont ceux de ${\displaystyle {\mathcal {A}}}$ et ses états terminaux ceux de ${\displaystyle {\mathcal {B}}}$. Formellement, ${\displaystyle {\mathcal {C}}=(Q'\cup Q,{\mathcal {F}}\cup {\mathcal {F'}}\cup {\mathcal {G}},I,T')}$ avec ${\displaystyle {\mathcal {G}}=\{(q,a,i')\mid i'\in I',(q,a,t)\in {\mathcal {F}},t\in T\}}$.

Ces trois propriétés démontrent que tout ω-langage rationnel est reconnaissable par un automate de Büchi.

• Intersection : Soient ${\displaystyle {\mathcal {A}}=(Q_{A},{\mathcal {F}}_{A},I_{A},T_{A})}$ et ${\displaystyle {\mathcal {B}}=(Q_{B},{\mathcal {F}}_{B},I_{B},T_{B})}$ reconnaissant respectivement les langages ${\displaystyle L_{A}}$ et ${\displaystyle L_{B}}$. Un automate reconnaissant l'intersection ${\displaystyle L_{A}\cap L_{B}}$ est construit de la manière suivante : ${\displaystyle {\mathcal {C}}=\{Q_{A}\times Q_{B}\times \{0,1,2\},Q_{A}\times Q_{b}\times \{0\},{\mathcal {F}},T\}}$, où les transitions de ${\displaystyle {\mathcal {F}}}$ copient celles de ${\displaystyle {\mathcal {F_{A}}}}$ et ${\displaystyle {\mathcal {F_{B}}}}$ pour les deux premières composantes, et changent la troisième composante de 0 en 1 quand un état de ${\displaystyle T_{A}}$ apparaît dans la première composante, de 1 en 2 quand ensuite un état de ${\displaystyle T_{B}}$ apparaît dans la deuxième composantes, et retourne en 0 immédiatement après. Dans un calcul, un 2 apparaît infiniment souvent en troisième composante si et seulement un état de ${\displaystyle T_{A}}$ et un état de ${\displaystyle T_{B}}$ apparaissent infiniment souvent en première et en deuxième composante. Donc, en choisissant pour états terminaux de ${\displaystyle Q_{A}\times Q_{b}\times \{2\}}$ on obtient un automate de Büchi au comportement désiré[7].

Les langages reconnus par des automates de Büchi sont fermés par complémentation. Büchi en a donné une démonstration en 1962[1]. Plus tard, d'autres constructions de l'automate reconnaissant les langages complémentaires ont été développées[8] - [9] - [10] - [11].

Les automates de Büchi sont équivalents aux automates de Muller, aux automates de Rabin, automates de Streett ou automates de parité. Cependant, ils différent par leur concision. Par exemple, les automates de Büchi sont exponentiellement plus concis que les automates de Rabin dans le sens suivant : il existe une famille de langages (L_n)_n=2.. sur l'alphabet {0, 1, #}, reconnaissable par des automates de Büchi non-déterministes de taille O(n) mais tout automate de Rabin non-déterministe équivalent doit être de taille au moins n![12].

Les automates de Büchi non déterministes représentent exactement les propriétés de la logique monadique de second ordre à un successeur (S1S), dites aussi propriétés ω-régulières[13]. La logique S1S est strictement plus expressive que la logique temporelle linéaire.

Il existe une condition duale à l'acceptation des automates de Büchi : il s'agit des automates co-Büchi. La condition d'acceptation est alors : une trace (ou calcul ou chemin infini) est réussie si et seulement si tout état apparaissant un nombre fini de fois est un état acceptant[14].

• Wolfgang Thomas, « Automata on infinite objects », dans : Jan Van Leeuwen (éditeur), Handbook of Theoretical Computer Science: Formal Models and Semantics, t. B, MIT Press, 1990, 1287 p. (ISBN 0-262-72015-9), p. 133-192
• Berndt Farwer, « ω-Automata », dans : Erich Grädel, Wolfgang Thomas et Thomas Wilke (éditeurs), Automata, logics, and infinite games : A guide to current research, Springer-Verlag, coll. « Lecture Notes in Computer Science » (n^o 2500),‎ 2002, viii+385 (ISBN 978-3-540-00388-5), p. 3-22.
• Samuel Eilenberg, Automata, Languages and Machines, Vol. A, Academic Press, coll. « Pure and Applied Mathematics » (n^o 58), 1974, xvi+451 (ISBN 978-0-12-234001-7), « Chap. XIV. Infinite Behavior of Finite Automata », p. 379-393.