Büchi-Automat

Der Büchi-Automat (nach dem Schweizer Mathematiker Julius Richard Büchi) ist eine spezielle Form des ω-Automaten. Dieser Automatentyp kann benutzt werden, um sowohl Sprachen über unendlichen Wörtern als auch über unendlichen 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 Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle A=\left(Q,\Sigma,\Delta,I,F\right)} wobei gilt:

• $Q$ ist eine endliche Menge von Zuständen, die Zustandsmenge
• Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \Sigma} ist eine endliche Menge von Symbolen, das Eingabealphabet
• Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \Delta} ist die Übergangsrelation mit Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \Delta \subseteq Q \times \Sigma \times Q}
• $I$ ist eine endliche Menge von Zuständen mit $I\subseteq Q$, die Startzustandsmenge
• Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle F} ist eine endliche Menge von Zuständen mit Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle F \subseteq Q} , die Endzustandsmenge

Deterministischer Büchi-Automat zur Worterkennung

Ein deterministischer Büchi-Automat (DBA) ist ein 5-Tupel Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle A=\left(Q,\Sigma,\delta,q_0,F\right)} wobei gilt:

• Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle Q} ist eine endliche Menge von Zuständen, die Zustandsmenge
• Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \Sigma} ist eine endliche Menge von Symbolen, das Eingabealphabet
• Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \delta} ist die Übergangsfunktion mit Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \delta\colon Q \times \Sigma \rightarrow Q}
• $q_{0}$ ist der Startzustand mit Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle q_0 \in Q}
• Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle F} ist eine endliche Menge von Zuständen mit Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle F \subseteq Q} , die Endzustandsmenge

Deterministische Büchi-Automaten sind nicht unter Komplementbildung abgeschlossen.

Akzeptanzverhalten

Ein unendliches Wort Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle w=a_1a_2a_3 \ldots } wird vom (nichtdeterministischen) Büchi-Automaten Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle A } akzeptiert genau dann, wenn für einen (deterministisch: den) zugehörigen (unendlichen) Pfad Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle 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 } gilt:

• Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle q_0 \in I }
• $(q_{i},a_{i+1},q_{i+1})\in \Delta$ für alle Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle i }
• es gibt unendlich viele $i$ mit Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle q_i \in F } .

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

Die von einem Büchi-Automaten Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle A } akzeptierte ω-Sprache (Menge unendlicher Wörter) ist Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle L_{\omega}(A)=\{w \in \Sigma^{\omega} \mid w \text{ wird von } A \text{ akzeptiert}\} } . Diese ω-Sprache heißt dann Büchi-erkennbar. Jede Büchi-erkennbare ω-Sprache kann durch Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \cup_{i=1}^m U_i V_i^{\omega} } dargestellt werden, wobei Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle U_i } und Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle V_i } reguläre Sprachen für alle Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle i } sind. Aufgrund dieses engen Zusammenhangs zu regulären Sprachen werden Büchi-erkennbare ω-Sprachen auch als ω-reguläre Sprachen bezeichnet. Damit ist der nichtdeterministische Büchi-Automat äquivalent zum Muller-Automaten, Rabin-Automaten, Streett-Automaten und zum Parity-Automaten.

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 Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle L=\{w\in\{a,b\}^{\omega}\backslash \{\epsilon\} \mid a\text{ kommt in }w \text{ nur endlich oft vor}\}} erkennt. Ein nichtdeterministischer Büchi-Automat für Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle L} kann dagegen wie folgt grafisch angegeben werden:

Büchi-Automaten zur Baumerkennung

Die Abkürzung BBA (englisch 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, dessen Knoten mit Symbolen aus dem Eingabealphabet Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \Sigma} beschriftet sind und bei dem jeder Knoten einen Ausgangsgrad Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle k} hat. Der Aufbau des Büchi-Automaten zur Baumerkennung entspricht dem des NBA, wobei jedoch die Übergangsrelation eine andere Form hat:

Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \Delta \subseteq Q \times \Sigma \times Q^k} .

Ein Lauf eines Büchi-Baumautomaten Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle A} auf einem Eingabebaum Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle t} ist ein Baum Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \rho} , der die gleichen Eigenschaften wie $t$ hat, bei dem die Knoten jedoch nicht mit Eingabesymbolen, sondern mit Zuständen beschriftet sind. Die Wurzel von $\rho$ ist mit einem Startzustand versehen, die restlichen Beschriftungen erfolgen gemäß der Übergangsrelation.

Akzeptanzverhalten

Ein unendlicher Baum Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle t} wird von einem Büchi-Baumautomaten Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle A} akzeptiert genau dann, wenn für einen Lauf Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \rho} von Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle A} auf $t$ gilt: Auf jedem unendlichen Pfad in Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \rho} 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 abgeschlossen. Unter Komplement ist sie hingegen nicht abgeschlossen, wie sich mit einer Variante des Pumping-Lemmas zeigen lässt.

Jeder Büchi-Baumautomat lässt sich in einen äquivalenten 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ätsbaumautomaten, welche äquivalent zu MBAs sind.

Co-Büchi-Automaten

Ein (deterministischer) Co-Büchi-Automat ist ein 5-Tupel Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle A=\left(Q,\Sigma,\delta,q_0,F\right)} 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 Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle w=a_1a_2a_3 \ldots } wird vom (deterministischen) Büchi-Automaten bzw. Co-Büchi-Automaten $A=\left(Q,\Sigma ,\delta ,q_{0},F\right)$ akzeptiert genau dann, wenn für den zugehörigen eindeutigen Pfad $q_{0}\rightarrow q_{1}\rightarrow q_{2}\rightarrow q_{3}\ldots$ gilt

• $\forall i\exists j\geq i$ mit Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle q_j\in F} (Büchi-Automat)
• Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \exists i\forall j\geq i} mit Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle q_j\in F} (Co-Büchi-Automat)

Literatur

• Wolfgang Thomas: Automata on Infinite Objects. In: 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.