Rabin-Automat

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].

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

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

Ein deterministischer Rabin-Automat (DRA) ist ein 5-Tupel ${\displaystyle {\mathcal {A}}=\left(Q,\Sigma ,\delta ,q_{0},{\mathcal {R}}\right)}$ wobei gilt:

• ${\displaystyle Q}$ ist eine endliche Menge von Zuständen, die Zustandsmenge,
• ${\displaystyle \Sigma }$ ist eine endliche Menge von Symbolen, das Eingabealphabet,
• ${\displaystyle \delta }$ ist die Übergangsfunktion mit ${\displaystyle \delta \colon Q\times \Sigma \rightarrow Q}$,
• ${\displaystyle q_{0}}$ ist der Startzustand mit ${\displaystyle q_{0}\in Q}$,
• ${\displaystyle {\mathcal {R}}\subseteq 2^{Q}\times 2^{Q}}$ ist eine Familie von Paaren von Zustandsmengen.

Die Mächtigkeit von ${\displaystyle {\mathcal {R}}}$ wird als Index des Automaten bezeichnet.^[1]

Ein unendliches Wort ${\displaystyle w=a_{1}a_{2}\ldots }$ wird vom deterministischen Rabin-Automaten ${\displaystyle {\mathcal {A}}}$ akzeptiert genau dann, wenn es für den zugehörigen unendlichen Pfad ${\displaystyle \pi =q_{0}\;{\xrightarrow {a_{1}}}\;q_{1}\;{\xrightarrow {a_{2}}}\;q_{2}\;\ldots }$ ein Paar ${\displaystyle (L,U)\in {\mathcal {R}}}$ gibt mit

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

Eine Definition mit umgekehrter Bedeutung des Paars ${\displaystyle (L,U)}$ ist ebenso möglich.^[3]

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 ${\displaystyle n\cdot (k+1)}$ 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 ${\displaystyle {\mathcal {A}}}$ der Größe n und vom Index k gibt es einen deterministischen Streett-Automaten ${\displaystyle {\overline {\mathcal {A}}}}$ der Größe n und vom Index k dessen Sprache komplementär zur Sprache von ${\displaystyle {\mathcal {A}}}$ ist: ${\displaystyle L({\overline {\mathcal {A}}})=\Sigma ^{\omega }\setminus L({\mathcal {A}})}$.^[1]

Des Weiteren gilt:

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

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

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.