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.

Définition formelle

Un automate de Muller (« non déterministe ») A est un quintuplet (Q, Σ, Δ, Q₀, F) où :

• Q est un ensemble fini, dont les éléments sont appelés les états de A ;
• Σ est un ensemble fini appelé l'alphabet de A ;
• Δ est une partie de Q × Σ × Q, relation de transition dont les éléments sont appelés les transitions de A (intuitivement, (q, a, q') ∈ Δ s'interprète comme « on peut passer de l'état q à l'état q' en lisant la lettre a ») ;
• Q₀ est une partie de Q, dont les éléments sont appelés les états initiaux ;
• F est un ensemble d'ensembles d'états : formellement, F ⊆ P(Q) où P(Q) est l'ensemble des parties de Q. F définit la condition d'acceptation : A accepte exactement les exécutions dans lesquelles l'ensemble des états rencontrés infiniment souvent est un élément de F.

Dans un automate de Muller déterministe, la relation de transition Δ est remplacée par une fonction de transition δ : Q × Σ → Q qui renvoie un état et l'ensemble des états initiaux Q₀ est remplacé par un état initial q₀ (élément de Q). Généralement, le terme automate de Muller désigne un automate de Muller non déterministe (c'est-à-dire pas nécessairement déterministe).

Exemples

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 automates de parité, les automates de Streett, les automates de Rabin. L'équivalence entre automate de Muller et automate de Büchi non déterministe constitue le théorème de McNaughton (en), démontré en premier par Robert McNaughton en 1966.

Références

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

Ouvrages de référence

• (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)