Automate sur les mots infinis

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é.

Définition

Comme pour les automates finis, un automate sur les mots infinis sur un alphabet ${\displaystyle A}$ est un quadruplet ${\displaystyle {\mathcal {A}}=(Q,{\mathcal {F}},I,T)}$, où :

• ${\displaystyle Q}$ est un ensemble fini d'états,
• ${\displaystyle {\mathcal {F}}\subseteq Q\times A\times Q}$ est l'ensemble des transitions,
• ${\displaystyle I\subseteq Q}$ est l'ensemble des états initiaux,
• et ${\displaystyle T\subseteq Q}$ est un ensemble d'états finals ou terminaux.

Souvent on suppose qu'il existe un seul état initial^[1]. 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}}$. Il n'a pas d'état d'arrivée, et le calcul est réussi et le mot est accepté ou reconnu en fonction de la condition d'acceptation de la famille d'automates considéré. La condition d'acceptation remplace alors l'ensemble des états terminaux.

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}$.

Pour un automate déterministe, la fonction de transition ${\displaystyle \delta :Q\times A\to Q}$ est la fonction partielle définie par : ${\displaystyle \delta (q,a)=q'}$ si ${\displaystyle (q,a,q')}$ est une transition.

Condition d'acceptation

Pour un calcul ${\displaystyle c}$, on note ${\displaystyle {\rm {Inf}}(c)}$ l'ensemble des états qui apparaissent une infinité de fois dans ${\displaystyle c}$. C'est ce concept qui permet de formuler les conditions d'acceptation.

Automate de Büchi

La condition d'acceptation est : ${\displaystyle {\mathcal {A}}}$ accepte un mot infini si et seulement s'il est l'étiquette d'un calcul ${\displaystyle c}$ pour lequel ${\displaystyle {\rm {Inf}}(c)}$ contient au moins un état final, donc tel que ${\displaystyle {\rm {Inf}}(c)\cap T\neq \emptyset }$.

Automate de Rabin

Un automate de Rabin comporte un ensemble ${\displaystyle \Omega }$ de couples ${\displaystyle (E,F)}$ d'ensembles d'états. La condition d'acceptation est : ${\displaystyle {\mathcal {A}}}$ accepte un mot infini si et seulement s'il est l'étiquette d'un calcul pour lequel il existe un couple ${\displaystyle (E,F)}$ de ${\displaystyle \Omega }$ tel que ${\displaystyle {\rm {Inf}}(c)\cap E=\emptyset }$ et ${\displaystyle {\rm {Inf}}(c)\cap F\neq \emptyset }$.

Automate de Streett

Un automate de Streett comporte un ensemble ${\displaystyle \Omega }$ de couples ${\displaystyle (E,F)}$ d'ensembles d'états. La condition d'acceptation est : ${\displaystyle {\mathcal {A}}}$ accepte un mot infini si et seulement s'il est l'étiquette d'un calcul tel que pour tout couple ${\displaystyle (E,F)}$ de ${\displaystyle \Omega }$, on a ${\displaystyle {\rm {Inf}}(c)\cap E\neq \emptyset }$ et ${\displaystyle {\rm {Inf}}(c)\cap F=\emptyset }$.

La condition de Streett est la négation de la condition de Rabin. Un automate de Streett déterministe accepte donc exactement le complément de l'ensemble accepté par l'automate de Rabin déterministe pour le même ensemble ${\displaystyle \Omega }$.

Automate de parité

Un automate de parité est un automate dont les états sont numérotés, disons ${\displaystyle Q=\{0,1,\ldots ,n\}}$. La condition d'acceptation est : ${\displaystyle {\mathcal {A}}}$ accepte un mot infini si et seulement s'il est l'étiquette d'un calcul tel que le plus petit des entiers dans ${\displaystyle {\rm {Inf}}(c)}$ est pair.

Automate de Muller

Un automate de Muller comporte une famille ${\displaystyle {\mathcal {M}}}$ d'ensembles d'états. La condition d'acceptation est : ${\displaystyle {\mathcal {A}}}$ accepte un mot infini si et seulement s'il est l'étiquette d'un calcul tel que ${\displaystyle {\rm {Inf}}(c)}$ est dans ${\displaystyle {\mathcal {M}}}$.

Tout automate de Büchi peut être vue comme un automate de Muller: Il suffit de prendre comme famille ${\displaystyle {\mathcal {M}}}$ l'ensemble des parties de ${\displaystyle Q}$ contenant au moins un état final. Réciproquement, pour tout automate de Muller à ${\displaystyle n}$ états et ${\displaystyle m}$ ensembles d’acceptation, il existe un automate de Büchi équivalent avec au plus ${\displaystyle n+mn2^{n}}$ états^[2]. De manière similaire, les automates de Rabin, de Streett et les automates de parité peuvent être vus comme des automates de Muller.

Exemple

L'automate ci-contre reconnaît l'ensemble des 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 }}$. En effet, pour chaque mot de ${\displaystyle \{a,b\}^{*}b^{\omega }}$, il y a une exécution qui boucle dans l'état q₁ et q₁ est acceptant.

On peut montrer qu'il n'existe pas d'automate de Büchi déterministe qui accepte le langage ${\displaystyle \{a,b\}^{*}b^{\omega }}$. Ainsi, les automates de Büchi déterministes sont strictement moins puissants que les automates de Büchi non déterministes.

Puissance d'expression

Un langage de mots infinis ou ω-langage est un ensemble de mots infinis sur un alphabet donné. La puissance d'expression d'un ω-automate est mesurée par la classe de tous ω-langages qui peuvent être reconnus par un automate de cette classe. Les automates de Büchi non déterministes, de parité, de Rabin, de Streett et de Muller reconnaissent tous les mêmes langages, qui sont les ensembles rationnels de mots infinis ou ω-langages rationnels. On peut montrer que les automates de parité, de Rabin, de Streett et de Muller déterministes reconnaissent également ces mêmes langages, contrairement donc aux automates de Büchi déterministes. Il en résulte en particulier que la classe des ω-langages est fermée par complémentation.

Notes et références

Notes

Références

• 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.

• (en) Wolfgang Thomas, « Automata on infinite objects », dans Jan Van Leeuwen (éditeur), Handbook of Theoretical Computer Science, vol. B : Formal Models and Semantics, Elsevier, 1990 (ISBN 978-0444880741), p. 133-192

• (en) Dominique Perrin et Jean-Éric Pin, Infinite Words : Automata, Semigroups, Logic and Games, Amsterdam/Boston, Elsevier, 2004, 538 p. (ISBN 978-0-12-532111-2, présentation en ligne)

Annexes

Articles connexes

• Théorie des automates
• Langage rationnel
• Automate à pile
• Automate d'arbres

Liens externes

• Paritosh K. Pandya, Automata on Infinite Words
• Yann Pequignot, Automates, Langages et Logique, École polytechnique fédérale de Lausanne, 2009

• (en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « ω-automaton » (voir la liste des auteurs).

• Portail de l'informatique théorique