Büchi automaton

Definition

Let $\Sigma$ be an alphabet and let $\Sigma^\omega$ be the set of infinite words $a_0 a_1 a_2 \cdots$ with all $a_i \in \Sigma$. A (nondeterministic) Büchi automaton is a tuple $B = (Q, \Sigma, \Delta, q_0, F)$ where:

1. $Q$ is a finite set of states;
2. $\Delta \colon Q \times \Sigma \to \mathcal{P}(Q)$ is the transition function, with values in the power set of $Q$;
3. $q_0 \in Q$ is the initial state;
4. $F \subseteq Q$ is the set of accepting states.

A run of $B$ on $\alpha = a_0 a_1 \cdots \in \Sigma^\omega$ is a sequence $r_0 r_1 r_2 \cdots$ of states with $r_0 = q_0$ and $r_{i+1} \in \Delta(r_i, a_i)$ for all $i \ge 0$. The run is accepting when $r_i \in F$ for infinitely many $i$. The automaton $B$ accepts $\alpha$ when some run of $B$ on $\alpha$ is accepting. Its language is the set $L_\omega(B) \subseteq \Sigma^\omega$ of the infinite words it accepts. $B$ is deterministic when every set $\Delta(q, a)$ has exactly one element.