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: un mot infini est accepté par l'automate s'il est l'étiquette d'un chemin qui passe une infinité de fois par les états d'un des ensembles d'états terminaux distingués.

Ce type d'automate a été introduit par David E. Muller en 1963. Ces automates - déterministes ou non - ont le même pouvoir de reconnaissance que les automates de Büchi.

Propriétés

Les automates de Muller déterministes et non déterministes reconnaissent les mêmes ensembles de mots infinis que les automates de Büchi non déterministes, les automate de parité, les automate de Streett, les automate de Rabin. L'équivalence entre automate de Müller et automate de Büchi non déterministe constitue le théorème de McNaughton (en).

Références

(en) David E. Muller, « Infinite sequences and finite machines », dans Proceedings of the Fourth Annual Symposium on Switching Circuit Theory and Logical Design, IEEE, 1963, p. 3-16 

Ouvrages de 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) Dominique Perrin et Jean-Éric Pin, Infinite Words: Automata, Semigroups, Logic and Games, Elsevier, 2004 (ISBN 978-0-12-532111-2)