„Rabin-Automat“ – Versionsunterschied
[gesichtete Version] | [gesichtete Version] |
K tk k |
D3rT!m (Diskussion | Beiträge) Hinweis auf mögliche andere Definition; Kleinigkeiten |
||
Zeile 6: | Zeile 6: | ||
Ein nichtdeterministischer Rabin-Automat (NRA) ist ein 5-Tupel <math>\mathcal{A} = \left(Q,\Sigma,\Delta,I,\mathcal{R}\right)</math> wobei gilt: |
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>Q</math> ist eine endliche Menge von Zuständen, die Zustandsmenge, |
||
* <math>\Sigma</math> ist eine endliche Menge von Symbolen, das Eingabealphabet |
* <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>\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>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 |
* <math>\mathcal{R} \subseteq 2^Q \times 2^Q</math> ist eine Familie von Paaren von Zustandsmengen. |
||
=== Deterministischer Rabin-Automat zur Worterkennung === |
=== 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: |
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>Q</math> ist eine endliche Menge von Zuständen, die Zustandsmenge, |
||
* <math>\Sigma</math> ist eine endliche Menge von Symbolen, das Eingabealphabet |
* <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>\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>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 |
* <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 |
Die Mächtigkeit von <math>\mathcal{R}</math> wird als Index des Automaten bezeichnet.<ref name=":0">{{Literatur |Autor=Martin Hofmann, Martin Lange |Titel=Automatentheorie und Logik |Sammelwerk=eXamen.press |Verlag=Springer-Verlag |Datum=2011 |ISBN=978-3-642-18089-7}}</ref> |
||
=== Akzeptanzverhalten === |
=== Akzeptanzverhalten === |
||
Zeile 27: | Zeile 27: | ||
Ein unendliches [[Wort (Theoretische Informatik)|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 unendliches [[Wort (Theoretische Informatik)|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 |
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 |
* <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 |
* <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>{{Literatur |Autor=[[Orna Kupferman]] |Titel=Automata Theory and Model Checking |Hrsg=[[Edmund Clarke]], [[Thomas Henzinger]], Helmut Veith, Roderick Bloem |Sammelwerk=Handbook of Model Checking |Verlag=Springer |Datum=2018 |DOI=10.1007/978-3-319-10575-8_4 |Seiten=122}}</ref> |
|||
=== Verhältnis zu Büchi-, Streett- und Muller-Automaten === |
=== Verhältnis zu Büchi-, Streett- und Muller-Automaten === |
||
Zeile 34: | Zeile 35: | ||
* Für jeden NBA der Größe n gibt es einen äquivalenten NRA mit Index 1 und gleicher Größe n.<ref name=":0" /> |
* 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 [[Potenzmengenkonstruktion|Potzenautomatenkonstruktion]] lässt sich zeigen, dass: |
Durch verallgemeinerte [[Potenzmengenkonstruktion|Potzenautomatenkonstruktion]] lässt sich zeigen, dass: |
||
* Zu jedem NBA gibt es einen DRA mit identischer [[Formale Sprache|Sprache]]<ref>{{Internetquelle |autor=Markus Holzer; Erstellt von Benjamin Gufler |url=http://home.in.tum.de/~gufler/files/afsb.pdf |titel=Automaten, formale Sprachen und Berechenbarkeit |abruf=2017-02-03 |format=PDF |sprache=de}}</ref> |
* Zu jedem NBA gibt es einen DRA mit identischer [[Formale Sprache|Sprache]].<ref>{{Internetquelle |autor=Markus Holzer; Erstellt von Benjamin Gufler |url=http://home.in.tum.de/~gufler/files/afsb.pdf |titel=Automaten, formale Sprachen und Berechenbarkeit |abruf=2017-02-03 |format=PDF |sprache=de}}</ref> |
||
Eine Rabinbedingung lässt sich jedoch auch in eine Büchi-Bedingung umwandeln, es gilt: |
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" /> |
* 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-Automat]]en. Daher lassen sich Deterministische Rabin- und Streett-Automaten leicht ineinander komplementieren und es gilt: |
Die Akzeptanzbedingung des Rabin-Automaten ist dual zur Akzeptanzbedingung des [[Streett-Automat]]en. 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 (Mengenlehre)|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" /> |
* 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 (Mengenlehre)|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: |
Des Weiteren gilt: |
||
*Jeder DRA ist zu einem deterministischen [[Muller-Automat]]en (DMA) äquivalent und umgekehrt. |
*Jeder DRA ist zu einem deterministischen [[Muller-Automat]]en (DMA) äquivalent und umgekehrt. |
Aktuelle Version vom 29. Dezember 2022, 21:24 Uhr
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 | Quelltext bearbeiten]Nichtdeterministischer Rabin-Automat zur Worterkennung
[Bearbeiten | Quelltext 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 | Quelltext 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 | Quelltext 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 | Quelltext 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:
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.
Quellen und Weblinks
[Bearbeiten | Quelltext bearbeiten]- 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
[Bearbeiten | Quelltext bearbeiten]- ↑ 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.
- ↑ 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.
- ↑ 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.
- ↑ Markus Holzer; Erstellt von Benjamin Gufler: Automaten, formale Sprachen und Berechenbarkeit. (PDF) Abgerufen am 3. Februar 2017.