🍽 🥨 MensaarLecker -- A beloved tool to find out Mensa Ladies' favourite menu using Selenium🥨 🍽

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

---

Please cite the source for reprints, feel free to verify the sources cited in the article, and point out any errors or lack of clarity of expression. You can comment in the comments section below or email to GreenMeeple@yahoo.com