Automate de Büchi
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 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 a été défini par le mathématicien Julius Richard Büchi[1].

Les automates de Büchi déterministes et non déterministes ne sont pas équivalents. Par exemple, il n'existe pas d'automate de Büchi déterministe qui reconnaît les mots infinis sur deux lettres UNIQ5b34c70a3c73d26d-math-00000006-QINU et b qui ne contiennent qu'un nombre fini de lettres b, c'est-à-dire l'ensemble {a,b} * bω, alors que cet ensemble est reconnu par un automate de Büchi non déterministe à deux états.

Les ensembles de mots infinis reconnus par les automates de Büchi sont les ensembles de la forme

\bigcup_1^mU_iV_i^\omega

où les UiVi et Vi sont des langages rationnels pour tout i.

Ceci signifie que les automates de Büchi sont équivalents aux automates de Muller, aux automates de Rabin, automates de Streett ou automates de parité.

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. La logique S1S est strictement plus expressive que la logique temporelle linéaire.

Notes

  1. J.R. Büchi. On a decision method in restricted second order arithmetic. In Proc. International Congress on Logic, Method, and Philosophy of Science. 1960, pages 1–12, Stanford, 1962. Stanford University Press.

Référence

(en) Wolfgang Thomas, Automata on infinite objects, dans Handbook of Theoretical Computer Science : Formal Models and Semantics, tome B (Jan Van Leeuwen, éd.), MIT Press (ISBN 0-262-72015-9)


Wikimedia Foundation. 2010.

Contenu soumis à la licence CC-BY-SA. Source : Article Automate de Büchi de Wikipédia en français (auteurs)

Regardez d'autres dictionnaires:

  • Automate De Büchi — Un automate de Büchi est un automate fini avec une condition d acceptation particulière : une trace est acceptée si et seulement si elle passe un nombre infini de fois par au moins un état acceptant. Les automates de Büchi déterministes et… …   Wikipédia en Français

  • Automate de Buchi — Automate de Büchi Un automate de Büchi est un automate fini avec une condition d acceptation particulière : une trace est acceptée si et seulement si elle passe un nombre infini de fois par au moins un état acceptant. Les automates de Büchi… …   Wikipédia en Français

  • Automate de büchi — Un automate de Büchi est un automate fini avec une condition d acceptation particulière : une trace est acceptée si et seulement si elle passe un nombre infini de fois par au moins un état acceptant. Les automates de Büchi déterministes et… …   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 — 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 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

  • Buchi — Büchi Cette page d’homonymie répertorie les différents sujets et articles partageant un même nom. Büchi est un patronyme : Alfred Büchi, ingénieur suisse, en 1905, il a dépose un brevet de turbocompresseur. Albert Büchi, cycliste suisse,… …   Wikipédia en Français

Share the article and excerpts

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