Der Rabin-Automat ist eine spezielle Form des ω-Automaten. Sie sind benannt nach ihrem Erfinder Michael O. Rabin[1], der damit 1969 erstmals endliche Automaten auf unendliche Wörter verallgemeinerte[2][1].

Rabin-Automaten zur Worterkennung

Bearbeiten

Nichtdeterministischer Rabin-Automat zur Worterkennung

Bearbeiten

Ein nichtdeterministischer Rabin-Automat (NRA) ist ein 5-Tupel   wobei gilt:

  •   ist eine endliche Menge von Zuständen, die Zustandsmenge,
  •   ist eine endliche Menge von Symbolen, das Eingabealphabet,
  •   ist die Übergangsrelation mit  ,
  •   ist eine endliche Menge von Zuständen mit  , die Startzustandsmenge,
  •   ist eine Familie von Paaren von Zustandsmengen.

Deterministischer Rabin-Automat zur Worterkennung

Bearbeiten

Ein deterministischer Rabin-Automat (DRA) ist ein 5-Tupel   wobei gilt:

  •   ist eine endliche Menge von Zuständen, die Zustandsmenge,
  •   ist eine endliche Menge von Symbolen, das Eingabealphabet,
  •   ist die Übergangsfunktion mit  ,
  •   ist der Startzustand mit  ,
  •   ist eine Familie von Paaren von Zustandsmengen.

Die Mächtigkeit von   wird als Index des Automaten bezeichnet.[1]

Akzeptanzverhalten

Bearbeiten

Ein unendliches Wort   wird vom deterministischen Rabin-Automaten   akzeptiert genau dann, wenn es für den zugehörigen unendlichen Pfad   ein Paar   gibt mit

  •  , d. h. alle Zustände aus   werden nur endlich oft besucht, und
  •  , d. h. mindestens ein Zustand aus   wird unendlich oft besucht.

Eine Definition mit umgekehrter Bedeutung des Paars   ist ebenso möglich.[3]

Verhältnis zu Büchi-, Streett- und Muller-Automaten

Bearbeiten

Das Akzeptanzverhalten eines nichtdeterministischen Rabin-Automaten (NRA) ist allgemeiner als eines nichtdeterministischen Büchi-Automaten (NBA), daher gilt:

  • Für jeden NBA der Größe n gibt es einen äquivalenten NRA mit Index 1 und gleicher Größe n.[1]

Durch verallgemeinerte Potzenautomatenkonstruktion lässt sich zeigen, dass:

  • Zu jedem NBA gibt es einen DRA mit identischer Sprache.[4]

Eine Rabinbedingung lässt sich jedoch auch in eine Büchi-Bedingung umwandeln, es gilt:

  • Für jeden NRA der Größe n und vom Index k gibt es einen äquivalenten NBA mit höchstens   Zuständen.[1]

Die Akzeptanzbedingung des Rabin-Automaten ist dual zur Akzeptanzbedingung des Streett-Automaten. Daher lassen sich Deterministische Rabin- und Streett-Automaten leicht ineinander komplementieren und es gilt:

  • Für jeden DRA   der Größe n und vom Index k gibt es einen deterministischen Streett-Automaten   der Größe n und vom Index k dessen Sprache komplementär zur Sprache von   ist:  .[1]

Des Weiteren gilt:

  • Jeder DRA ist zu einem deterministischen Muller-Automaten (DMA) äquivalent und umgekehrt.
Bearbeiten

Einzelnachweise

Bearbeiten
  1. a b c d e f Martin Hofmann, Martin Lange: Automatentheorie und Logik. In: eXamen.press. Springer-Verlag, 2011, ISBN 978-3-642-18089-7.
  2. Michael O. Rabin: Decidability of second-order theories and automata on infinite trees. Band 141, Nr. 5. Trans. Amer. Math. Soc., 1969, S. 1–35.
  3. Orna Kupferman: Automata Theory and Model Checking. In: Edmund Clarke, Thomas Henzinger, Helmut Veith, Roderick Bloem (Hrsg.): Handbook of Model Checking. Springer, 2018, S. 122, doi:10.1007/978-3-319-10575-8_4.
  4. Markus Holzer; Erstellt von Benjamin Gufler: Automaten, formale Sprachen und Berechenbarkeit. (PDF) Abgerufen am 3. Februar 2017.