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 U_iV_i et V_i 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)