Mullers Automat

In der theoretischen Informatik und insbesondere in der Automatentheorie ist ein Müller- Automat ein endlicher Automat , der unendliche Wörter erkennt und mit einer Familie von Mengen unterschiedlicher Endzustände ausgestattet ist. Der Erkennungsmodus ist wie folgt: Ein unendliches Wort wird vom Automaten akzeptiert, wenn es die Bezeichnung eines Pfades ist, der unendlich oft durch die Zustände eines der Sätze von unterscheidbaren Endzuständen verläuft.

Diese Art von Automaten wurde von eingeführt David E. Muller in 1963 . Diese Automaten - deterministisch oder nicht - haben die gleiche Erkennungskraft wie die Büchi-Automaten .

Formale Definition

Ein Müller-Automat ("nicht deterministisch") A ist ein Fünffach ( Q , Σ, Δ, Q 0 , F ), wobei:

• Q ist eine endliche Menge, deren Elemente die Zustände von A genannt werden  ;
• Σ ist eine endliche Menge, die als Alphabet von A bezeichnet wird  ;
• Δ ist ein Teil von Q × Σ × Q , einer Übergangsbeziehung, deren Elemente als Übergänge von A bezeichnet werden (intuitiv wird ( q , a , q ' ) ∈ Δ als "wir können vom Zustand q in den Zustand q' übergehen " interpretiert. durch Lesen des Buchstabens a  ”);
• Q 0 ist ein Teil von Q , dessen Elemente als Anfangszustände bezeichnet werden  ;
• F ist eine Menge von Mengen von Zuständen: Formal ist F ⊆ P ( Q ), wobei P ( Q ) die Menge von Teilmengen von Q ist . F definiert die Annahmebedingung: Um akzeptieren genau Ausführungen , in denen alle auftretenden Zustände unendlich oft ein Element F .

In einem deterministischen Müller-Automaten wird die Übergangsrelation Δ durch eine Übergangsfunktion δ ersetzt: Q × Σ → Q, die einen Zustand zurückgibt, und die Menge der Anfangszustände Q 0 wird durch einen Anfangszustand q 0 (Element von Q ) ersetzt. Im Allgemeinen bezeichnet der Begriff Müller-Automat einen nicht deterministischen Müller-Automaten (dh nicht unbedingt deterministisch).

Beispiele

Eigenschaften

Automaten Müller deterministisch und nicht deterministisch erkennen die gleichen Sätze von unendlichen Wörtern wie Büchi Automaten nicht deterministisch, die Paritätsautomaten , die Automaten Streett , die Rabin-Automaten . Die Äquivalenz zwischen PLC Muller und nicht deterministischem Büchi-Automaten ist der Satz von McNaughton  (in) , der erstmals 1966 von Robert McNaughton demonstriert wurde .

Verweise

(en) David E. Muller , "  Unendliche Sequenzen und endliche Maschinen  " , Proceedings of the Fourth Annual Symposium on Switching Circuit Theory and Logical Design , IEEE,1963, p.  3-16

Nachschlagewerke

(en) Wolfgang Thomas , „Automaten über unendliche Objekte“ , in Jan Van Leeuwen (Herausgeber), Handbook of Theoretical Computer Science , vol.  B: Formale Modelle und Semantik , Elsevier,1990( ISBN  978-0444880741 ) , p.  133-192

(en) Dominique Perrin und Jean-Éric Pin , Unendliche Wörter: Automaten, Halbgruppen, Logik und Spiele , Amsterdam / Boston, Elsevier,2004538  p. ( ISBN  978-0-12-532111-2 , Online-Präsentation )