Rabin-Automat

Der Rabin-Automat ist eine spezielle Form des ω-Automaten. Sie sind benannt nach ihrem Erfinder Michael O. Rabin<ref name=":0" />, der damit 1969 erstmals endliche Automaten auf unendliche Wörter verallgemeinerte<ref>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. </ref><ref name=":0" />.

Rabin-Automaten zur Worterkennung

Nichtdeterministischer Rabin-Automat zur Worterkennung

Ein nichtdeterministischer Rabin-Automat (NRA) ist ein 5-Tupel <math>\mathcal{A} = \left(Q,\Sigma,\Delta,I,\mathcal{R}\right)</math> wobei gilt:

<math>Q</math> ist eine endliche Menge von Zuständen, die Zustandsmenge,
<math>\Sigma</math> ist eine endliche Menge von Symbolen, das Eingabealphabet,
<math>\Delta</math> ist die Übergangsrelation mit <math>\Delta \subseteq Q \times \Sigma \times Q</math>,
<math>I</math> ist eine endliche Menge von Zuständen mit <math>I \subseteq Q</math>, die Startzustandsmenge,
<math>\mathcal{R} \subseteq 2^Q \times 2^Q</math> ist eine Familie von Paaren von Zustandsmengen.

Deterministischer Rabin-Automat zur Worterkennung

Ein deterministischer Rabin-Automat (DRA) ist ein 5-Tupel <math>\mathcal{A} = \left(Q,\Sigma,\delta,q_0,\mathcal{R}\right)</math> wobei gilt:

<math>Q</math> ist eine endliche Menge von Zuständen, die Zustandsmenge,
<math>\Sigma</math> ist eine endliche Menge von Symbolen, das Eingabealphabet,
<math>\delta</math> ist die Übergangsfunktion mit <math>\delta\colon Q \times \Sigma \rightarrow Q</math>,
<math>q_0</math> ist der Startzustand mit <math>q_0 \in Q</math>,
<math>\mathcal{R} \subseteq 2^Q \times 2^Q</math> ist eine Familie von Paaren von Zustandsmengen.

Die Mächtigkeit von <math>\mathcal{R}</math> wird als Index des Automaten bezeichnet.<ref name=":0">Martin Hofmann, Martin Lange: Automatentheorie und Logik. In: eXamen.press. Springer-Verlag, 2011, ISBN 978-3-642-18089-7. </ref>

Akzeptanzverhalten

Ein unendliches Wort <math>w=a_1a_2 \ldots</math> wird vom deterministischen Rabin-Automaten <math>\mathcal{A}</math> akzeptiert genau dann, wenn es für den zugehörigen unendlichen Pfad <math>\pi = q_0 \; \xrightarrow{a_1} \; q_1 \; \xrightarrow{a_2} \; q_2 \; \ldots</math> ein Paar <math>(L, U) \in \mathcal{R}</math> gibt mit

<math>\operatorname{Inf}(\pi) \cap L = \emptyset</math>, d. h. alle Zustände aus <math>L</math> werden nur endlich oft besucht, und
<math>\operatorname{Inf}(\pi) \cap U \neq \emptyset</math>, d. h. mindestens ein Zustand aus <math>U</math> wird unendlich oft besucht.

Eine Definition mit umgekehrter Bedeutung des Paars <math>(L,U)</math> ist ebenso möglich.<ref>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. </ref>

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

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.<ref name=":0" />

Durch verallgemeinerte Potzenautomatenkonstruktion lässt sich zeigen, dass:

Zu jedem NBA gibt es einen DRA mit identischer Sprache.<ref>Markus Holzer; Erstellt von Benjamin Gufler: Automaten, formale Sprachen und Berechenbarkeit. (PDF) Abgerufen am 3. Februar 2017. </ref>

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 <math>n \cdot (k+1)</math> Zuständen.<ref name=":0" />

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 <math>\mathcal{A}</math> der Größe n und vom Index k gibt es einen deterministischen Streett-Automaten <math>\overline\mathcal{A}</math> der Größe n und vom Index k dessen Sprache komplementär zur Sprache von <math>\mathcal{A}</math> ist: <math>L(\overline\mathcal{A})= \Sigma^\omega \setminus L(\mathcal{A})</math>.<ref name=":0" />

Des Weiteren gilt:

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

Quellen und Weblinks

Martin Hofmann, Martin Lange: Automatentheorie und Logik. In: eXamen.press. Springer-Verlag, 2011, ISBN 978-3-642-18089-7.
Vorlesungsmitschrift zu "Automaten, formale Sprachen und Berechenbarkeit", gehalten von Prof. Dr. Markus Holzer, Wintersemester 2004/05 – Kapitel 2.5.3 (PDF; 461 kB)

Einzelnachweise