AGV 3.5 -- Büchi's Characterization Theorem

Previous chapter: Closure Properties of the Büchi-recognizable languages (Concatenations)

This is a learning note of a course in CISPA, UdS. Taught by Bernd Finkbeiner

We are now ready to prove Büchi’s Characterization Theorem, a result from 1962.

$\textbf{Theorem 3.6. }\text{(Büchi’s Characterization Theorem) }\newline\textit{An $\omega$-language is Büchi-recognizable iff it is $\omega$-regular.}$

Explained in Human language

p.s. Büchi-recognizable means the language can be described by a Büchi automata.

$”\Leftarrow”$
We have to prove if the language is $\omega$-regular, then it is Büchi-recognizable.
In section 3.2, we learn that an $\omega$-regular language contains 3 operators:

• union of $\omega$-regular languages, $W_1+W_2$ (proved by Theorem 3.2),
• infinite concatenation of a non-empty regular language $E^\omega$ (proved by Theorem 3.4), and
• concatenation of regular languages and $\omega$-regular language $E\cdot W$ (proved by Theorem 3.5)

$”\Rightarrow”$
We have to prove if the language is Büchi-recognizable, then it is $\omega$-regular.
Here, we try to construct a Büchi-recognizable using all $\omega$-regular operators.

We begin by constructing a regular language $W_{q,q’}$. Words of the language $w$ is accepted by some finite-word automata, with a pair of state $q,q’\in Q$ being the initial and accepting states respectively.

Then we try to prove that a Büchi-recognizable language $\mathcal{L}(\mathcal{A})$ equals to the regular language concatenates (3.5) with the infinite concatenated, non-empty (3.4) starting from the previous accepting state. That is $W_{q,q’}\cdot(W_{q’,q’}\setminus\lbrace\varepsilon\rbrace)^\omega$.

On top of that, we do a set union (3.2) for each pair of initial and accepting states $q,q’\in Q$, that is $\bigcup_{q\in I,q’\in F}$

Therefore, now we only need to prove that $\mathcal{L}(\mathcal{A})=\bigcup_{q\in I,q’\in F}W_{q,q’}\cdot(W_{q,q’}\setminus\lbrace\varepsilon\rbrace)^\omega$.

For the word $\alpha$ from L.H.S, it reaches $q’\in F$ infinitely often. We can thus seperate into $r:q\xrightarrow{w_0}q’\xrightarrow{w_1}q’\xrightarrow{w_2}\dots$
The $w$ here refers the word to reach $q’$. We know that Büchi automata is non-empty so $|w_i|>0$ when $i>0$.
Therefore, $w_0$ will be a word from $W_{q,q’}$ and the rest will be words for $(W_{q’,q’}\setminus\lbrace\varepsilon\rbrace)^\omega$ because they reach the accepting state $q’\in F$.

For the word $w_0w_1w_2\dots$ from R.H.S, where $w_0$ refers to $W_{q,q’}$ and the rest refers to $(W_{q’,q’}\setminus\lbrace\varepsilon\rbrace)^\omega$.
This is accepted by $\mathcal{L}(\mathcal{A})$ because it reaches the accepting state $q’\in F$ infinitely often.

Formal Proof

$”\Leftarrow”$
Follows from the closure properties of the Büchi-recognizable languages established by Theorems 3.2, 3.4, 3.5.

$”\Rightarrow”$
Given a Büchi automaton $\mathcal{A}$, we consider for each pair $q,q’\in Q$ the regular language
$$
W_{q,q’} = \lbrace w\in\Sigma^*\mid \text{finite-word automaton } (\Sigma,Q,\lbrace q\rbrace,T,{q’}) \text{ accepts }w\rbrace.
$$
We claim that $\mathcal{L}(\mathcal{A})=\bigcup_{q\in I,q’\in F}W_{q,q’}\cdot(W_{q,q’}\setminus\lbrace\varepsilon\rbrace)^\omega$. The claim is proven as follows.

$\mathcal{L}(\mathcal{A})\subseteq\bigcup_{q\in I,q’\in F}W_{q,q’}\cdot(W_{q,q’}\setminus\lbrace\varepsilon\rbrace)^\omega$: Let $\alpha\in\mathcal{L}(\mathcal{A})$. Then there is an accpeting run $r$ of $\mathcal{A}$ on $\alpha$, which begins at some $q=r(0)\in I$ and visits some $q’\in F$ infinitely often:

$$
r:q\xrightarrow{w_0}q’\xrightarrow{w_1}q’\xrightarrow{w_2}\dots
$$

where $w_i\in\Sigma^*$ for all $i\ge 0$, $|w_i|>0$ for all $i>0$ and $\alpha=w_0w_1w_2\dots$ The notation $q_0\xrightarrow{w}q_{k+1}$ for some finite word $w=w(0)w(1)\dots w(k)$ means that there exist states $q_1,\dots,q_k\in Q$ s.t. $(q_i,w(i),q_{i+1})\in T$ for all $0\leq i \leq k$. Since $w_0\in W_{q,q’}$ and $w_k\in W_{q’,q’}$ for $k>0$, we have that $\alpha \in W_{q,q’}\cdot W_{q’,q’}^\omega$ for some $q\in I,q’\in F$.

$\mathcal{L}(\mathcal{A})\supseteq\bigcup_{q\in I,q’\in F}W_{q,q’}\cdot(W_{q,q’}\setminus\lbrace\varepsilon\rbrace)^\omega$: Let $\alpha=w_0w_1w_2\dots$ with $w_0\in W_{q,q’}$ and $w_k\in W_{q’,q’}$ for some $q\in I,q’\in F$ and for all $k>0$. Then the run:

$$
r:q\xrightarrow{w_0}q’\xrightarrow{w_1}q’\xrightarrow{w_2}\dots
$$

exists and is aceepting because $q’\in F$. It follows that $\alpha\in\mathcal{L}(\mathcal{A})$.

---

Next chapter: Deterministic vs. Nondeterministic Büchi Automata

Further Reading: Büchi automaton