Büchi machine

The Büchi automaton (after the Swiss mathematician Julius Richard Büchi ) is a special form of the ω automaton . This type of automaton can be used to recognize languages over infinite words as well as over infinite trees .

Büchi machines for word recognition

Non-deterministic Büchi machine for word recognition

A nondeterministic Büchi automaton (NBA) is a 5-tuple where: ${\displaystyle A=\left(Q,\Sigma ,\Delta ,I,F\right)}$

• ${\displaystyle Q}$ is a finite set of states, the state set
• ${\displaystyle \Sigma }$ is a finite set of symbols, the input alphabet
• ${\displaystyle \Delta }$ is the transition relation with ${\displaystyle \Delta \subseteq Q\times \Sigma \times Q}$
• ${\displaystyle I}$is a finite set of states with , the starting state set ${\displaystyle I\subseteq Q}$
• ${\displaystyle F}$is a finite set of states with , the final state set ${\displaystyle F\subseteq Q}$

Deterministic Büchi machine for word recognition

A deterministic Büchi machine (DBA) is a 5-tuple where: ${\displaystyle A=\left(Q,\Sigma ,\delta ,q_{0},F\right)}$

• ${\displaystyle Q}$ is a finite set of states, the state set
• ${\displaystyle \Sigma }$ is a finite set of symbols, the input alphabet
• ${\displaystyle \delta }$ is the transition function with ${\displaystyle \delta \colon Q\times \Sigma \rightarrow Q}$
• ${\displaystyle q_{0}}$ is the start state with ${\displaystyle q_{0}\in Q}$
• ${\displaystyle F}$is a finite set of states with , the final state set ${\displaystyle F\subseteq Q}$

Deterministic Büchi automata are not closed with complement formation .

The possibility of power set construction , i.e. H. the algorithm for turning a nondeterministic into a deterministic automaton can not be applied to Büchi automata . The set of languages ​​that can be recognized by deterministic Büchi automata is really smaller than the set of languages ​​that can be recognized by nondeterministic Büchi automata.

For example, there is no deterministic Büchi automaton over that recognizes the language , i.e. the language of all ω-words that contain only finitely many a. ${\displaystyle \Sigma ^{\omega }=\left\{a,b\right\}^{\omega }}$ ${\displaystyle \Sigma ^{*}\{b^{\omega }\}}$

A non-deterministic Büchi automaton can, however, be given.

Acceptance behavior

An infinite word is accepted by the (nondeterministic) Büchi automata if and only if for a (deterministic: the) associated (infinite) path holds ${\displaystyle w=a_{1}a_{2}a_{3}\ldots }$ ${\displaystyle A}$ ${\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 }$

• ${\displaystyle q_{0}\in I}$
• ${\displaystyle (q_{i},a_{i+1},q_{i+1})\in \Delta }$ for all ${\displaystyle i}$
• there are infinitely many with ${\displaystyle i}$ ${\displaystyle q_{i}\in F}$

Less formally this means: If a final state is passed through infinitely often, the Büchi machine accepts the input word.

The ω-language (set of infinite words) accepted by a Büchi automaton is . ${\displaystyle A}$ ${\displaystyle L_{\omega }(A)=\{w\in \Sigma ^{\omega }\mid w{\text{ wird von }}A{\text{ akzeptiert}}\}}$

This ω-language is then called Büchi-recognizable.

Every Büchi-recognizable ω-language can be represented by, where and are regular languages for all . Because of this close connection to regular languages, Büchi-recognizable ω-languages ​​are also referred to as ω-regular languages. ${\displaystyle \cup _{i=1}^{m}U_{i}V_{i}^{\omega }}$ ${\displaystyle U_{i}}$ ${\displaystyle V_{i}}$ ${\displaystyle i}$

The nondeterministic Büchi automaton is therefore equivalent to the Muller automaton , Rabin automaton , Streett automaton and to the parity automaton .

Büchi machines for tree recognition

The abbreviation BBA ( English BTA ) denotes a non-deterministic Büchi automaton for tree recognition; deterministic Büchi tree automata are usually not considered.

The input is an infinite, rooted tree , the nodes of which are labeled with symbols from the input alphabet and for which each node has the starting degree. ${\displaystyle \Sigma }$ ${\displaystyle k}$

The structure of the Büchi machine for tree recognition corresponds to that of the NBA, but the transition relation has a different form:

${\displaystyle \Delta \subseteq Q\times \Sigma \times Q^{k}}$.

A run of a Büchi tree automaton on an input tree is a tree that has the same properties as , but in which the nodes are not labeled with input symbols but with states. The root of is provided with a start state, the remaining labels are made according to the transition relation. ${\displaystyle A}$ ${\displaystyle t}$ ${\displaystyle \rho }$ ${\displaystyle t}$ ${\displaystyle \rho }$

Acceptance behavior

An infinite tree is accepted by a Büchi tree automaton if and only if the following applies to a run from on : On every infinite path in there are infinitely many final states. ${\displaystyle t}$ ${\displaystyle A}$ ${\displaystyle \rho }$ ${\displaystyle A}$ ${\displaystyle t}$ ${\displaystyle \rho }$

The trees accepted by a Büchi tree automaton form a Büchi recognizable tree language. The class of Büchi-recognizable tree languages ​​is completed under union . However , it is not closed under complement , as can be shown with a variant of the pumping lemma .

Every Büchi tree automat can be converted into an equivalent Muller tree automat (MBA). Since the class of the Muller-recognizable tree languages ​​is closed under complement, Büchi tree automata are weaker than MBAs and as parity tree automata , which are equivalent to MBAs.

Co-Büchi machines

A (deterministic) Co-Büchi automaton is a 5-tuple and differs from a deterministic Büchi automaton only in the acceptance behavior. While a Büchi automaton accepts a word if an end state is visited again and again, a Co-Büchi automaton only accepts a word if, from a certain point on, only end states are visited. ${\displaystyle A=\left(Q,\Sigma ,\delta ,q_{0},F\right)}$

If you write this down somewhat more formally, you can see that the existential quantifier and the universal quantifier are swapped. An infinite word is from the (deterministic) Büchi automata or co-Büchi automata accepted if and only if the associated unique path applies ${\displaystyle w=a_{1}a_{2}a_{3}\ldots }$ ${\displaystyle A=\left(Q,\Sigma ,\delta ,q_{0},F\right)}$ ${\displaystyle q_{0}\rightarrow q_{1}\rightarrow q_{2}\rightarrow q_{3}\ldots }$

• ${\displaystyle \forall i\exists j\geq i}$with (Büchi machine) ${\displaystyle q_{j}\in F}$
• ${\displaystyle \exists i\forall j\geq i}$with (Co-Büchi machine) ${\displaystyle q_{j}\in F}$

literature

• Wolfgang Thomas: Automata on Infinite Objects. In: Jan van Leeuwen (Ed.): Handbook of Theoretical Computer Science. Volume B: Formal Models and Semantics. Elsevier Science Publishers et al., Amsterdam et al. 1990, ISBN 0-444-88074-7 , pp. 133-164.