Voir la source de Automate de Büchi

[[File:Automate de Buchi.jpg|thumb|Automate de Büchi non déterministe reconnaissant les mots infinis contenant un nombre fini de <math>a</math>, c'est-à-dire l'ensemble <math>\{a,b\}^*b^\omega</math>.]]
En [[informatique théorique]], un '''automate de Büchi''' est un [[ω-automate]] ou [[automate fini]] opérant sur des [[Mot infini|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]]<ref name=":0">
{{article|auteur1=Julius R. Büchi
|titre=On a decision method in restricted second order arithmetic
|journal=Proc. International Congress on Logic, Method, and Philosophy of Science (1960)
|pages=1-12|année=1962
|éditeur=Stanford University Press}}.</ref>.

== Définition ==
Un ''automate de Büchi'' sur un [[alphabet]] <math>A</math> est un [[ω-automate]] <math>\mathcal{A} = (Q, \mathcal{F}, I, T)</math>, où :
* <math>Q</math> est un [[ensemble fini]] d'''états'' ;
* <math>\mathcal{F}\subset Q\times A\times Q</math> est l'ensemble des ''transitions'' ;
* <math>I \subseteq Q</math> est l'ensemble des états ''initiaux'' ;
* <math>T \subseteq Q</math> est un ensemble d'états ''finals'' ou ''terminaux''<!-- Seulement dans le cas des mots finis ? : exemple : https://www.eleves.ens.fr/home/melotti/enseignement/buchi.pdf--> ou ''acceptants''.
Souvent on suppose que l'ensemble des états initiaux est composé d'un seul élément<ref>Par exemple : {{harvsp|Farwer|2002|p=}}.</ref>. 
Une transition <math>f=(p,a,q)</math> est composée d'un état de départ <math>p</math>, d'une étiquette <math>a</math> et d'un état d'arrivée <math>q</math>. Un ''calcul'' <math>c</math> (on dit aussi un ''chemin'' ou une ''trace'') est une suite infinie de transitions consécutives :
:<math>c=(p_0,a_1,p_1)(p_1,a_2,p_2)\cdots</math>
Son état de départ est <math>p_0</math>, son ''étiquette'' est le mot infini <math>a_1a_2\cdots a_n\cdots</math>. 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 <math>q</math>, et pour toute lettre <math>a</math>, il existe au plus une transition partant de <math>q</math> et portant l'étiquette <math>a</math>.

== Exemples ==
[[File:2-state Buchi automaton.svg|thumb|left|Automate de Büchi <math>\mathcal{A}</math> reconnaissant les mots infinis contenant un nombre infini de <math>a</math>.]]

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

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

[[File:Automate de Buchi3.jpg|thumb|upright=1.3|Automate de Büchi reconnaissant les mots infinis où chaque occurrence de <math>b</math> est précédé d'un nombre pair non nul de <math>a</math>.]]

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

== Déterminisme versus non-déterminisme ==
Les automates de Büchi déterministes sont strictement moins puissants que les automates de Büchi non déterministes<ref>{{Ouvrage|prénom1=Christel|nom1=Baier|prénom2=Joost-Pieter|nom2=Katoen|titre=Principles of Model Checking (Representation and Mind Series)|éditeur=The MIT Press|date=2008-05-31|pages totales=975|passage=p. 191|isbn=978-0-262-02649-9|isbn10=026202649X|isbn2=9780262026499|lire en ligne=http://dl.acm.org/citation.cfm?id=1373322|consulté le=2018-02-06}}</ref>{{,}}<ref>{{Ouvrage|prénom1=Erich|nom1=Grädel|prénom2=Wolfgang|nom2=Thomas|prénom3=Thomas|nom3=Wilke|titre=Automata logics, and infinite games|sous-titre=a guide to current research|éditeur=Springer-Verlag New York, Inc.|date=2002-01-01|pages totales=385|passage=p. 11, sous-section 1.4.1|isbn=978-3-540-00388-5|isbn10=3540003886|lire en ligne=http://dl.acm.org/citation.cfm?id=938135|consulté le=2018-02-12}}</ref>. 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 <math>a</math> et <math>b</math> qui ne contiennent qu'un nombre fini de lettres <math>a</math>, c'est-à-dire l'ensemble <math>\{a,b\}^*b^\omega</math>, 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 <math>F</math> son ensemble d'états d'acceptation. L'automate accepte le mot infini <math>b^\omega</math>, dont le calcul passe une première fois dans un état de <math>F</math> après la lecture d'un certain nombre positif, disons <math>n</math>, de lettres <math>b</math>. L'automate accepte aussi le mot infini <math>b^nab^\omega</math>, donc le calcul passe une deuxième fois par un état de <math>F</math> après disons <math>m</math> lettres <math>b</math>. L'automate accepte donc le mot <math>b^nab^mab^\omega</math>. De proche en proche, on construit un mot  <math>b^{n_1}ab^{n_2}ab^{n_3}ab\cdots</math>  contenant une infinité de lettres <math>a</math> et qui est accepté par l’automate, contradiction.

== Langages reconnus ==
Les ensembles de mots infinis reconnus par les automates de Büchi sont les [[mot infini#Ensemble rationnel de mots infinis | ensembles rationnels de mots infinis]] ou ω-langages rationnels, à savoir les ensembles de la forme
:<math>\bigcup_1^mU_iV_i^\omega</math><br />
où les <math>U_i</math> et <math>V_i</math> sont des [[langage rationnel|langages rationnels]] pour tout <math>i</math>, les <math>V_i</math> ne contenant pas le mot vide. Ces langages sont aussi appelés les ω-[[fermeture de Kleene]] des langages rationnels<ref name="Farwer">{{harvsp|Farwer|2002|p=6}}.</ref>. 

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 <math>W(p,q)</math> l’ensemble des mots finis reconnus avec <math>p</math> comme état initial et <math>q</math> comme état final, donc les mots qui sont étiquettes d’un chemin de <math>p</math> à <math>q</math>. Ces langages (de mots finis) sont rationnels. Un mot infini <math>x</math> 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 <math>q</math>, par lequel il passe une infinité de fois. Ceci est équivalent à dire que 
: <math>x\in W(q_0,q)W(q,q)^\omega</math>
pour un état initial <math>q_0</math>. En prenant la réunion sur tous les états initiaux et terminaux, on obtient la description indiquée{{refm|"Farwer"}}. 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<ref>{{harvsp|Thomas|1990|p=138-139}}.</ref>.

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  <math>W(q_0,q)W(q,q)</math> n’est pas vide.

== Propriétés de clôture ==

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 <math>\mathcal{A} = (Q_A, \mathcal{F}_A, I_A, T_A)</math> et <math>\mathcal{B} = (Q_B, \mathcal{F}_B, I_B, T_B)</math> reconnaissant respectivement les langages <math>L_A</math> et <math>L_B</math>. Un automate reconnaissant la réunion <math>L_A \cup L_B</math> s'obtient en faisant la réunion des deux automates. On suppose les ensembles d'états de <math>\mathcal{A}</math> et <math>\mathcal{B}</math> disjoints ; alors l’automate {{retrait|<math>\mathcal{C} = (Q_A\cup Q_B, \mathcal{F}_A\cup \mathcal{F}_B, I_A\cup I_B, T_A\cup T_B)</math>}} reconnaît la réunion.

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

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

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

* '''Intersection''' : Soient <math>\mathcal{A} = (Q_A, \mathcal{F}_A, I_A, T_A)</math> et <math>\mathcal{B} = (Q_B, \mathcal{F}_B, I_B, T_B)</math> reconnaissant respectivement les langages <math>L_A</math> et <math>L_B</math>. Un automate reconnaissant l'intersection <math>L_A \cap L_B</math> est construit de la manière suivante : 
{{retrait|<math>\mathcal{C} = \{Q_A\times Q_B \times\{0,1,2\},\mathcal{F},I_A\times I_b\times\{0\},T\}</math>,}}  où les transitions de <math>\mathcal{F}</math> copient celles de <math>\mathcal{F_A}</math> et <math>\mathcal{F_B}</math> pour les deux premières composantes, et changent la troisième composante de 0 en 1 quand un état de <math>T_A</math> apparaît dans la première composante, de 1 en 2 quand ensuite un état de  <math>T_B</math> 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 <math>T_A</math> et  un état de <math>T_B</math> apparaissent infiniment souvent en première et en deuxième composante. Donc, en choisissant pour états terminaux de <math>Q_A\times Q_b\times\{2\}</math> on obtient un automate de Büchi au comportement désiré<ref>{{harvsp|Thomas|1990|p=138}}.</ref>.

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<ref name=":0" />. Plus tard, d'autres constructions de l'automate reconnaissant les langages complémentaires ont été développées<ref>
{{article
|auteur=[[Robert McNaughton]]
|titre=Testing and generating infinite sequences by a finite automaton
|périodique=Information and Control
|volume=9|passage=521-530
|année=1966
|doi=10.1016/s0019-9958(66)80013-x}}.
</ref>{{,}}<ref>{{article|prénom1=A. P.|nom1=Sistla|prénom2=M. Y.|nom2=Vardi|lien auteur2=Moshe Vardi|prénom3=P.|nom3=Wolper|lien auteur3=Pierre Wolper|titre=The complementation problem for Büchi automata with applications to temporal logic|journal=[[Theoretical Computer Science]]|volume=49|pages=217–237|année=1987|doi=10.1016/0304-3975(87)90008-9}}.</ref>{{,}}<ref>{{article|prénom=S.|nom=Safra|lien auteur=Shmuel Safra|titre=On the complexity of ω-automata|journal=Proc. 29th IEEE [[Symposium on Foundations of Computer Science]], White Plains, New York|pages=319–327|date=October 1988}}.</ref>{{,}}<ref>{{article|prénom1=O.|nom1=Kupferman|prénom2=M. Y.|nom2=Vardi|lien auteur2=Moshe Vardi|titre=Weak alternating automata are not that weak|journal=[[ACM Transactions on Computational Logic]]|volume=2|numéro=2|pages=408–429|date=July 2001}}.</ref>.

== Lien avec les autres modes de reconnaissance ==

Les automates de Büchi sont équivalents aux [[automate de Muller|automates de Muller]], aux [[ω-automate|automates de Rabin]], [[ω-automate|automates de Streett]] ou [[ω-automate|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<sub>n</sub>)<sub>n=2..</sub> 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!<ref>{{Ouvrage|prénom1=Erich|nom1=Grädel|prénom2=Wolfgang|nom2=Thomas|prénom3=Thomas|nom3=Wilke|titre=Automata logics, and infinite games|sous-titre=a guide to current research|éditeur=Springer-Verlag New York, Inc.|date=2002-01-01|pages totales=385|passage=p. 18, Theorem 1.30.|isbn=978-3-540-00388-5|isbn10=3540003886|lire en ligne=http://dl.acm.org/citation.cfm?id=938135|consulté le=2018-02-12}}</ref>. 

Les automates de Büchi non déterministes représentent exactement les propriétés de la [[Logique monadique du second ordre|logique monadique de second ordre]] à un successeur (S1S), dites aussi propriétés ω-régulières<ref>{{harvsp|Thomas|1990|p=144-146}}.</ref>. La logique S1S est strictement plus expressive que la [[logique temporelle|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<ref>{{Ouvrage|titre=Complementing Büchi Automata|langue=anglais|lire en ligne=https://www.lrde.epita.fr/~sadegh/buchi-complementation-techrep.pdf|prénom1=Guillaume|nom1=Sadegh|auteur institutionnel=Laboratoire de Recherche et Développement de l’Epita|lieu= Le Kremlin-Bicêtre|tome=0903, révision 2073|nature ouvrage=Technical Report|année=2009|mois=mai}}</ref>.

== Algorithmique ==

=== Logique du temps linéaire et model checking ===
On utilise les automates de Büchi en [[vérification de modèles]] (model checking) où des questions algorithmiques se posent. Par exemple, savoir si le langage d'un automate de Büchi non-déterministe est vide se décide en temps linéaire<ref>{{Ouvrage|prénom1=Christel|nom1=Baier|prénom2=Joost-Pieter|nom2=Katoen|titre=Principles of Model Checking (Representation and Mind Series)|éditeur=The MIT Press|date=2008-05-31|pages totales=975|passage=p. 185, Th. 4.42|isbn=978-0-262-02649-9|isbn10=026202649X|isbn2=9780262026499|lire en ligne=http://dl.acm.org/citation.cfm?id=1373322|consulté le=2018-02-06}}</ref>. On peut traduire une formule de la [[logique temporelle linéaire]] (LTL) en un automate de Büchi, mais dont la taille est exponentielle en la taille de la formule LTL<ref>{{Ouvrage|prénom1=Christel|nom1=Baier|prénom2=Joost-Pieter|nom2=Katoen|titre=Principles of Model Checking (Representation and Mind Series)|éditeur=The MIT Press|date=2008-05-31|pages totales=975|isbn=978-0-262-02649-9|isbn10=026202649X|isbn2=9780262026499|lire en ligne=http://dl.acm.org/citation.cfm?id=1373322|consulté le=2018-02-07}}</ref>. Cette transformation peut servir à :
* décider le problème de satisfiabilité de LTL. Ce problème est [[PSPACE-complet]], mais voici un algorithme en temps exponentiel : construire un automate de Büchi équivalent à la formule LTL puis tester si son langage est vide ;
* Faire de la vérification de modèles (model checking). Pour cela, on construit l'automate de Büchi équivalent à la formule LTL et on fait le produit avec le système à vérifier. Le produit est un automate de Büchi et il faut tester si son langage est vide.
[[Fichier:Buchi generalise.svg|vignette|Transformation d'un automate de Büchi généralisé en un automate de Büchi classique.]]
La transformation d'une formule LTL en un automate de Büchi est généralement présenté avec un intermédiaire, appelé '''automate de Büchi généralisé''', où la condition d'acceptation est plus générale. Un automate de Büchi généralisé est comme un automate de Büchi, sauf que l'ensemble d'états terminaux <math>T \subseteq Q</math> est remplacé par une famille finie <math>\{T_1, \dots, T_k\}</math>  où <math>T_i \subseteq Q</math>. La condition d'acceptation devient : une trace (ou calcul ou chemin infini) est réussie si et seulement si pour tout i, elle passe un nombre infini de fois par au moins un état acceptant de <math>T_i</math>. Dans la figure ci-contre, l'automate du haut est un automate de Büchi correspondant à des mots sur l'alphabet {<math>\top</math>, cr1, cr2}. L'exemple provient de la propriété <math>\varphi</math> "infiniment souvent dans la [[section critique]] 1, et infiniment souvent dans la section critique 2". La lettre <math>\top</math> correspond à une section non critique, cr1 correspond à la section critique 1 et cr2 à la section critique 2. La famille <math>T \subseteq Q</math><nowiki> est {{q</nowiki><sub>1</sub>}, {q<sub>2</sub><nowiki>}}. Une exécution acceptante, doit passer infiniment souvent par q1 et infiniment souvent par q2. Cela correspond bien à la propriété </nowiki><math>\varphi</math>.

On transforme d'abord la formule LTL en un automate de Büchi généralisé (l'idée est que les états de l'automate sont les sous-ensemble maximaux consistants de sous-formules de la formule LTL). Par exemple, la propriété <math>\varphi</math> s'écrit en LTL : <math>GF cr_1 \land GF cr_2</math> (toujours dans le futur cr1 et toujours dans le futur cr2). L'automate généralisé est donné dans la figure ci-contre, automate du haut. On transforme alors cet automate en un automate de Büchi usuel : il est obtenu en faisant une copie de l'automate généralisé pour chaque sous-ensemble <math>T_i</math>. Dans l'exemple, l'automate est recopié deux fois : la première copie correspond à {q<sub>1</sub>} et la deuxième à {q<sub>2</sub>}. Une fois q<sub>1</sub> rencontré, on passe dans la seconde copie. Une fois q<sub>2</sub>' rencontré, on repasse dans la première copie. L'automate obtenu est un automate de Büchi classique est la condition d'acceptation est de passer une infinité de fois par q<sub>1</sub> ou q<sub>2</sub>'. Par construction, cette condition est équivalente à passer une infinité de fois dans q<sub>1</sub> et une infinité de fois dans q<sub>2</sub> dans l'automate généralisé.

Il existe des algorithmes efficaces en pratique pour construire un automate de Büchi équivalent à partir d'une formule LTL<ref>{{Article|langue=en|prénom1=Paul|nom1=Gastin|prénom2=Denis|nom2=Oddoux|titre=Fast LTL to Büchi Automata Translation|périodique=Computer Aided Verification|série=Lecture Notes in Computer Science|éditeur=Springer, Berlin, Heidelberg|date=2001-07-18|isbn=3540445854|doi=10.1007/3-540-44585-4_6|lire en ligne=https://link.springer.com/chapter/10.1007/3-540-44585-4_6|consulté le=2018-02-07|pages=53–65}}</ref>.

Il existe des algorithmes pour l'« apprentissage » d'un automate de Büchi<ref>{{article
|auteur1 = Yong Li |auteur2 = Yu-Fang Chen | auteur3 = Lijun Zhang | auteur4 = Depeng Liu
|titre = A novel learning algorithm for Büchi automata based on family of DFAs and classification trees
|journal= Information and Computation
|volume=281 |date = December 2021|numéro article = 104678
|doi=10.1016/j.ic.2020.104678}}.</ref>.

=== S1S et WS1S ===
Büchi<ref name=":0"/> a montré qu'il y a équivalence, pour tout langage de mots infinis L, entre :
* L est définissable par une propriété S1S ([[Logique monadique du second ordre|logique monadique de second ordre]] à un successeur) ;
* L est définissable par une propriété WS1S ([[Logique monadique du second ordre|logique monadique de second ordre]] à un successeur, dite "weak", c'est-à-dire que la quantification du second ordre porte sur les ensembles finis) ;
* L est reconnaissable par un automate de Büchi.
Les équivalences sont effectives : on transforme une formule S1S en un automate de Büchi. Ainsi, la logique S1S (et WS1S) est décidable. La logique S1S est de [[Problème non élémentaire|complexité non élémentaire]]<ref>{{Lien web|titre=Luke Ong - Automata, Logic and Games: Theory and Application 1. Büchi Automata and S1S|url=https://www.cs.ox.ac.uk/people/luke.ong/personal/talks/s1s.pdf}}</ref>.

== Notes ==
{{Références}}

== Références ==
* {{chapitre | auteur = Wolfgang Thomas | titre = Automata on infinite objects 
 | titre ouvrage = Handbook of Theoretical Computer Science: Formal Models and Semantics | tome = B 
 | auteur ouvrage = : Jan Van Leeuwen (éditeur)  | année =1990 | éditeur = {{Langue|en|MIT Press}} 
 | isbn = 0-262-72015-9 | pages totales = 1287 | passage = 133-192}} 
* {{chapitre | nom1=Farwer | prénom1=Berndt | titre=ω-Automata 
 | auteur ouvrage = : Erich Grädel, Wolfgang Thomas et Thomas Wilke (éditeurs) 
 | titre ouvrage =Automata, logics, and infinite games : A guide to current research
 | collection = Lecture Notes in Computer Science 
 |  numéro dans collection = 2500| éditeur = Springer-Verlag
 | année = 2002
 | pages totales = viii+385| isbn=978-3-540-00388-5 | passage = 3-22}}.
*{{Ouvrage
| id=EilenbergA
| prénom1=Samuel
| nom1=Eilenberg
| titre=Automata, Languages and Machines, Vol. A
| éditeur=Academic Press
| collection=Pure and Applied Mathematics
| numéro dans collection=58
| année=1974
| pages totales=xvi+451
| passage=379-393
| isbn=978-0-12-234001-7
| titre chapitre=Chap. XIV. Infinite Behavior of Finite Automata
}}.

{{Palette Automates finis et langages réguliers}}
{{Portail|informatique théorique}}

[[Catégorie:Calculabilité]]
[[Catégorie:Théorie des automates]]
[[Catégorie:Vérification de modèles]]