Büchi Automata
Nondeterministic Büchi Automata
A nondeterministic Büchi Automata (NBA) \(\mathcal{A}\) is a tuple \(\mathcal{A} = (\texttt{Q}, \Sigma, \delta, \texttt{Q}_0, \texttt{F})\) where:
- \(\texttt{Q}\) is a finite set of states,
- \(\Sigma\) is an alphabet,
- \(\delta : \texttt{Q} \times \Sigma \rightarrow 2^{\texttt{Q}}\) is a transition function,
- \(\texttt{Q}_0 \subseteq \texttt{Q}\) is a set of initial states, and
- \(\texttt{F} \subseteq \texttt{Q}\) is a set of accept (or: final) states, called the acceptance set.
A run for \(\sigma = A_0 A_1 A_2 \ldots \in \Sigma^\omega\) denotes an infinite sequence \(q_0 q_1 q_2 \ldots\) of states in \(\mathcal{A}\) such that \(q_0 \in \texttt{Q}_0\) and \(q_i \overset{\texttt{A}_i}{\longrightarrow} q_{i+1}\) for \(i \geq 0\). A run \(q_0 q_1 q_2 \ldots\) is accepting if \(q_i \in \texttt{F}\) for infinitely many indices \(i \in \mathbb{N}\). The accepted language of \(\mathcal{A}\) is
\[ \mathcal{L}(\mathcal{A}) = \{ \sigma \in \Sigma^\omega \,\mid\, \text{there exists an accepting run for } \sigma \text{ in } \mathcal{A} \} \]
The size of \(\mathcal{A}\), denoted by \(\lvert \mathcal{A} \rvert\), is defined as the number of states and transitions in \(\mathcal{A}\).
Deterministic Büchi Automata
Let \(\mathcal{A} = (\texttt{Q}, \Sigma, \delta, \texttt{Q}_0, \texttt{F})\) be an NBA. \(\mathcal{A}\) is called deterministic, if
\[ \lvert \texttt{Q}_0 \rvert \leq 1 \text{ and } \lvert \delta(q, A) \rvert \leq 1 \]
for all \(q \in \texttt{Q}\) and \(A \in \Sigma\). \(\mathcal{A}\) is total if \(\lvert \texttt{Q}_0 \rvert = 1\) and \(\lvert \delta(q, A) \rvert = 1\) for all \(q \in \texttt{Q}\) and \(A \in \Sigma\).