Automate sur les mots infinis


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, déterministe ou non, qui accepte des mots infins. Comme un tel automate ne s'arrête pas, les conditions d'acceptation sont plus évoluées que dans le cas des automates sur les mots finis.

Les automates sur les mots infinis servent à modéliser des calculs qui ne sont pas censés se terminer, comme le comportement d'un système d'exploitation, ou d'un système de contrôle. Pour de tels systèmes, on eput spécifier des propriétés comme « chaque requête sera suivie d'une réponse » ou sa négation « il existe un 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.

Les classes d'automates sur les mots infinis incluent 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, sauf les automates de Büchi déterministes qui reconnaissent seulement une sous-famille, , 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é.

Sommaire

Définition

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

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

Une transition f = (p,a,q) est composée d'un état de départ p, d'une étiquette a et d'un état d'arrivée q. Un calcul c (on dit aussi un chemin ou une trace) est une suite infinie de transitions consécutives:

c=(p_0,a_1,p_1)(p_1,a_2p_2)\cdots

Son état de départ est p0, son étiquette est le mot infini a_1a_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 q, et pour toute lettre a, il existe au plus une transition partant de q et portant l'étiquette a.

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

Condition d'acceptation

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

Automate de Büchi

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

Automate de Rabin

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

Automate de Streett

Un automate de Streett comporte un ensemble Ω de couples (E,F) d'ensembles d'états. La condition d'acceptation est: \mathcal{A} accepte un mot infini si et seulement s'il est l'étiquette d'un calcul tel que pour tout couple (E,F) de Ω, on a {\rm Inf}(c)\cap E\ne\emptyset et {\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 Ω.

Automate de parité

Un automate de parité est un automate dont les états sont numéroté, disons Q=\{0,1,\ldots,n\}. La condition d'acceptation est: \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 Inf(c) est pair.

Automate de Muller

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


Tout automate de Büchi peut être vue comme un automate de Muller: Il suffit de prendre comme famille \mathcal{M} l'ensemble des parties de Q contenant au moins un état final. De manière similaire, les automates de Rabin, de Streett et les automates de parité peuvent être vus comme des automates de Muller.

Références

  • (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) Erich Grädel, Wolfgang Thomas and Thomas Wilke (éditeurs), Automata, logics, and infinite games. A guide to current research, Springer-Verlag, coll. « Lecture Notes in Computer Science » (no 2500), 2002, viii+385 p. (ISBN 3-540-00388-6) 
  • (en) Dominique Perrin et Jean-Éric Pin, Infinite Words: Automata, Semigroups, Logic and Games, Elsevier, 2004 (ISBN 978-0-12-532111-2) 

Voir aussi

Lien externe



Wikimedia Foundation. 2010.

Contenu soumis à la licence CC-BY-SA. Source : Article Automate sur les mots infinis de Wikipédia en français (auteurs)

Regardez d'autres dictionnaires:

  • Automate fini — Pour les articles homonymes, voir Automate. Fig. 1 : Automate fini reconnaissant les écritures binaires des multiples de 3. Un automate fini (on dit parfois, par une traduction littér …   Wikipédia en Français

  • Automate cellulaire — À gauche, une règle locale simple : une cellule passe d un état (i) au suivant (i+1) dans le cycle d états dès que i+1 est présent dans au moins 3 cellules voisines. À droite, le résultat (complexe) de l application répétée de cette règle… …   Wikipédia en Français

  • Automate de Muller — En informatique théorique, et en particulier en théorie des automates, un automate de Muller est un automate fini reconnaissant des mots infinis, doté d une famille d ensemble d états terminaux distingués. Le mode de reconnaissance est le suivant …   Wikipédia en Français

  • Automate fini déterministe — Automate fini Pour les articles homonymes, voir Automate. Exemple d un diagramme d automate fini. Un automate fini (on dit parfois machine …   Wikipédia en Français

  • Automate fini non déterministe — Automate fini Pour les articles homonymes, voir Automate. Exemple d un diagramme d automate fini. Un automate fini (on dit parfois machine …   Wikipédia en Français

  • Automate fini non déterministe généralisé — Automate fini Pour les articles homonymes, voir Automate. Exemple d un diagramme d automate fini. Un automate fini (on dit parfois machine …   Wikipédia en Français

  • Automate Fini — Pour les articles homonymes, voir Automate. Exemple d un diagramme d automate fini. Un automate fini (on dit parfois machine …   Wikipédia en Français

  • Automate déterministe à états fini — Automate fini Pour les articles homonymes, voir Automate. Exemple d un diagramme d automate fini. Un automate fini (on dit parfois machine …   Wikipédia en Français

  • Automate de Büchi — non déterministe reconnaissant les mots infinis contenant un nombre fini le a En informatique théorique, un automate de Büchi est un automate fini acceptant des mots infinis, avec une condition d acceptation particulière : une trace (ou… …   Wikipédia en Français

  • Lemme d'itération pour les langages algébriques — Le Lemme d itération pour les langages algébriques, aussi connu sous le vocable Lemme de Bar Hillel, Perles et Shamir, donne une condition de répétition nécessaire pour les langages algébriques. Sa version simplifiée pour les langages rationnels… …   Wikipédia en Français


Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”

We are using cookies for the best presentation of our site. Continuing to use this site, you agree with this.