imported>Vanished user 8491027: Sektion Eigenschaften eingefügt und Ausdrucksstärke NBA vs. DBA hinter Akzeptanzverhalten gesetzt, da Akzeptanzverhalten bekannt sein muss, um diesen Part zu verstehen. Die im Beispiel angegebene Sprache etwas vereinfacht und leeres Wort ausgeschlossen, damit grafischer NBA übereinstimmt. Ebenso Absätze die vorher nur aus einzelnen Sätzen bestanden zusammengefügt (siehe Wikipedia Style-Guide).

2020-11-07T11:39:29Z

Sektion Eigenschaften eingefügt und Ausdrucksstärke NBA vs. DBA hinter Akzeptanzverhalten gesetzt, da Akzeptanzverhalten bekannt sein muss, um diesen Part zu verstehen. Die im Beispiel angegebene Sprache etwas vereinfacht und leeres Wort ausgeschlossen, damit grafischer NBA übereinstimmt. Ebenso Absätze die vorher nur aus einzelnen Sätzen bestanden zusammengefügt (siehe Wikipedia Style-Guide).

Neue Seite

Der '''Büchi-Automat''' (nach dem Schweizer Mathematiker [[Julius Richard Büchi]]) ist eine spezielle Form des [[ω-Automat]]en. Dieser Automatentyp kann benutzt werden, um sowohl [[Formale Sprache|Sprachen]] über unendlichen [[Wort (Theoretische Informatik)|Wörtern]] als auch über unendlichen [[Baum (Graphentheorie)|Bäumen]] zu erkennen.

== Büchi-Automaten zur Worterkennung ==
=== Nichtdeterministischer Büchi-Automat zur Worterkennung ===
Ein nichtdeterministischer Büchi-Automat (NBA) ist ein 5-Tupel <math>A=\left(Q,\Sigma,\Delta,I,F\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>F</math> ist eine endliche Menge von Zuständen mit <math>F \subseteq Q</math>, die Endzustandsmenge

=== Deterministischer Büchi-Automat zur Worterkennung ===
Ein deterministischer Büchi-Automat (DBA) ist ein 5-Tupel <math>A=\left(Q,\Sigma,\delta,q_0,F\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>F</math> ist eine endliche Menge von Zuständen mit <math>F \subseteq Q</math>, die Endzustandsmenge

Deterministische Büchi-Automaten sind '''nicht''' unter [[Komplement (Mengenlehre)|Komplementbildung]] abgeschlossen.

=== Akzeptanzverhalten ===
Ein unendliches Wort <math> w=a_1a_2a_3 \ldots </math> wird vom (nichtdeterministischen) Büchi-Automaten <math> A </math> akzeptiert genau dann, wenn für einen (deterministisch: den) zugehörigen (unendlichen) Pfad <math> q_0\quad \begin{smallmatrix}a_1 \\ \rightarrow \\ A\end{smallmatrix}\quad q_1 \quad\begin{smallmatrix}a_2 \\ \rightarrow \\ A\end{smallmatrix}\quad q_2\quad \begin{smallmatrix}a_3 \\ \rightarrow \\ A\end{smallmatrix}\quad q_3 \quad\ldots </math> gilt:
* <math> q_0 \in I </math>
* <math> (q_i, a_{i+1}, q_{i+1}) \in \Delta </math> für alle <math> i </math>
* es gibt unendlich viele <math> i </math> mit <math> q_i \in F </math>.

Weniger formal bedeutet das: Wird ein Endzustand unendlich oft durchlaufen, dann akzeptiert der Büchi-Automat das Eingabewort.

Die von einem Büchi-Automaten <math> A </math> akzeptierte ω-Sprache (Menge unendlicher Wörter) ist
<math> L_{\omega}(A)=\{w \in \Sigma^{\omega} \mid w \text{ wird von } A \text{ akzeptiert}\} </math>. Diese ω-Sprache heißt dann Büchi-erkennbar. Jede Büchi-erkennbare ω-Sprache kann durch <math> \cup_{i=1}^m U_i V_i^{\omega} </math> dargestellt werden, wobei <math> U_i </math> und <math> V_i </math> [[reguläre Sprache]]n für alle <math> i </math> sind. Aufgrund dieses engen Zusammenhangs zu regulären Sprachen werden Büchi-erkennbare ω-Sprachen auch als [[omega-regulär|ω-reguläre]] Sprachen bezeichnet. Damit ist der nichtdeterministische Büchi-Automat äquivalent zum [[Muller-Automat]]en, [[Rabin-Automat]]en, [[Streett-Automat]]en und zum [[Parity-Automat]]en.

=== Eigenschaften ===
Die Möglichkeit der [[Potenzmengenkonstruktion]], d. h. der Algorithmus, um aus einem nichtdeterministischen einen deterministischen Automaten zu machen, ist auf Büchi-Automaten '''nicht''' anwendbar. Die Menge der durch deterministische Büchi-Automaten erkennbaren Sprachen ist '''echt kleiner''' als die Menge der durch nichtdeterministische Büchi-Automaten erkennbaren Sprachen. Zum Beispiel gibt es keinen deterministischen Büchi-Automaten, welcher die Sprache <math>L=\{w\in\{a,b\}^{\omega}\backslash \{\epsilon\} \mid a\text{ kommt in }w \text{ nur endlich oft vor}\}</math> erkennt. Ein nichtdeterministischer Büchi-Automat für <math>L</math> kann dagegen wie folgt grafisch angegeben werden:

[[Datei:Buechie01.PNG|nichtdeterministischer Büchi-Automat für die Sprache aller ω-Wörter, die nur endlich viele a enthalten]]

== Büchi-Automaten zur Baumerkennung ==
Die Abkürzung BBA ({{enS|''BTA''}}) bezeichnet einen nichtdeterministischen Büchi-Automaten zur Baumerkennung; deterministische Büchi-Baumautomaten werden in der Regel nicht betrachtet. Als Eingabe dient ein unendlicher, gewurzelter [[Baum (Graphentheorie)|Baum]], dessen Knoten mit Symbolen aus dem Eingabealphabet <math>\Sigma</math> beschriftet sind und bei dem jeder Knoten einen [[Ausgangsgrad]] <math>k</math> hat. Der Aufbau des Büchi-Automaten zur Baumerkennung entspricht dem des NBA, wobei jedoch die Übergangsrelation eine andere Form hat:

<math>\Delta \subseteq Q \times \Sigma \times Q^k</math>.

Ein Lauf eines Büchi-Baumautomaten <math>A</math> auf einem Eingabebaum <math>t</math> ist ein Baum <math>\rho</math>, der die gleichen Eigenschaften wie <math>t</math> hat, bei dem die Knoten jedoch nicht mit Eingabesymbolen, sondern mit Zuständen beschriftet sind. Die Wurzel von <math>\rho</math> ist mit einem Startzustand versehen, die restlichen Beschriftungen erfolgen gemäß der Übergangsrelation.

=== Akzeptanzverhalten ===
Ein unendlicher Baum <math>t</math> wird von einem Büchi-Baumautomaten <math>A</math> akzeptiert genau dann, wenn für einen Lauf <math>\rho</math> von <math>A</math> auf <math>t</math> gilt: Auf jedem unendlichen Pfad in <math>\rho</math> kommen unendlich viele Endzustände vor. Die durch einen Büchi-Baumautomaten akzeptierten Bäume bilden eine Büchi-erkennbare Baumsprache. Die Klasse der Büchi-erkennbaren Baumsprachen ist unter [[Vereinigung (Mengenlehre)|Vereinigung]] abgeschlossen. Unter [[Komplement (Mengenlehre)|Komplement]] ist sie hingegen nicht abgeschlossen, wie sich mit einer Variante des [[Pumping-Lemma]]s zeigen lässt.

Jeder Büchi-Baumautomat lässt sich in einen äquivalenten [[Muller-Automat#Muller-Automat zur Baumerkennung|Muller-Baumautomaten]] (MBA) umwandeln. Da die Klasse der muller-erkennbaren Baumsprachen unter Komplement abgeschlossen ist, sind Büchi-Baumautomaten schwächer als MBAs und als [[Paritätsbaumautomat]]en, welche äquivalent zu MBAs sind.

== Co-Büchi-Automaten ==
Ein (deterministischer) Co-Büchi-Automat ist ein 5-Tupel <math>A=\left(Q,\Sigma,\delta,q_0,F\right)</math> und unterscheidet sich von einem deterministischen Büchi-Automaten nur durch das Akzeptanzverhalten. Während ein Büchi-Automat ein Wort akzeptiert, falls immer wieder ein Endzustand besucht wird, so akzeptiert ein Co-Büchi-Automat ein Wort nur, wenn ab einem gewissen Punkt nur noch Endzustände besucht werden. Schreibt man dies etwas formaler auf, so sieht man, dass der Existenzquantor und der Allquantor vertauscht werden. Ein unendliches Wort <math> w=a_1a_2a_3 \ldots </math> wird vom (deterministischen) Büchi-Automaten bzw. Co-Büchi-Automaten <math>A=\left(Q,\Sigma,\delta,q_0,F\right)</math> akzeptiert genau dann, wenn für den zugehörigen eindeutigen Pfad <math>q_0\rightarrow q_1\rightarrow q_2\rightarrow q_3 \ldots </math>
gilt
* <math>\forall i\exists j\geq i</math> mit <math>q_j\in F</math> (Büchi-Automat)
* <math>\exists i\forall j\geq i</math> mit <math>q_j\in F</math> (Co-Büchi-Automat)

== Literatur ==
* Wolfgang Thomas: ''Automata on Infinite Objects.'' In: [[Jan van Leeuwen (Informatiker)|Jan van Leeuwen]] (Hrsg.): ''Handbook of Theoretical Computer Science.'' Band B: ''Formal Models and Semantics.'' Elsevier Science Publishers u. a., Amsterdam u. a. 1990, ISBN 0-444-88074-7, S. 133–164.

{{SORTIERUNG:Buchiautomat}}
[[Kategorie:Automatentheorie]]

Büchi-Automat - Versionsgeschichte