Previous chapter: $\omega$-regular language
This is a learning note of a course in CISPA, UdS. Taught by Bernd Finkbeiner
In the following we will refer to the languages recognized by Büchi automata simply as Büchi-recognizable languages.
Büchi’s characterization theorem states that the $\omega$-regular languages are exactly Büchi-recognizable languages.
To prepare for the proof of Büchi’s theorem, we establish several closure properties of the Büchi-recognizable languages.
Closure Properties of Language Union
$\textbf{Construction 3.1. } \text{Let }L_1\text{ and }L_2\text{ be }\omega\text{-languages recognized by the Büchi automata}\newline\mathcal{A}_1=(\Sigma,Q_1,I_1,T_1,\small\text{BÜCHI}\normalsize (F_1))\text{ and }\mathcal{A}_2 = (\Sigma,Q_2,I_2,T_2,\small\text{BÜCHI}\normalsize (F_2))\text{, respectively.}\newline\text{We construct}\mathcal{A}_\cup=(\Sigma,Q_\cup,I_\cup,T_\cup,\small\text{BÜCHI}\normalsize (F_\cup))\text{ with }\mathcal{L}(\mathcal{A}_\cup)=L_1\cup L_2\text{ as follows:}$
$\begin{array}{l}
\hspace{1cm} \cdot \ Q_\cup=Q_1\cup Q_2 \hspace{1cm}(\text{w.l.o.g we assume }Q_1\cap Q_2=\varnothing)\newline
\hspace{1cm} \cdot \ I_\cup=I_1\cup I_2 \ \hspace{1cm} \cdot \ T_\cup=T_1\cup T_2 \ \hspace{1cm} \cdot \ F_\cup=F_1\cup F_2 \newline
\end{array}$
The correctness of this construction is proven by the following theorem.
$\textbf{Theorem 3.2. } \textit{If $L_1$ and $L_2$ are Büchi-recognizable, then so is $L_1\cup L_2$.}$
Formal Proof
We prove that the Büchi automaton $\mathcal{A}_\cup$ built by $\mathcal{A}_1$ and $\mathcal{A}_2$ indeed recognizes the union of the languages of the two automata.
$\mathcal{L}(\mathcal{A}_\cup)\subseteq\mathcal{L}(\mathcal{A}_1)\cup\mathcal{L}(\mathcal{A}_2):$
For $\alpha\in\mathcal{L}(\mathcal{A}_\cup)$, we have an accepting run $r=r(0)r(1)r(2)\dots$ of $\mathcal{A}_\cup$ on $\alpha$.
If $r(0)\in I_1$, then $r$ is an accepting run of $\mathcal{A}_1$, otherwise $r(0)\in I_2$ and $r$ is an accepting run of $\mathcal{A}_2$.
$\mathcal{L}(\mathcal{A}_\cup)\supseteq\mathcal{L}(\mathcal{A}_1)\cup\mathcal{L}(\mathcal{A}_2):$
For $i\in\lbrace 1,2\rbrace$ and $\alpha\in\mathcal{L}(\mathcal{A}_i)$, there is an accepting run $r$ of $\mathcal{A}_i$. The run $r$ is also an accepting run of $\mathcal{A}_\cup$.
Closure Properties of Language Intersection
As we will see later, the Büchi-recognizable languages are closed under complement.
The closure under complement and union implies the closure under intersection $(\mathcal{A}_\cap = (\mathcal{A’_1}\cup \mathcal{A’_2})’)$
Below, the automaton for the intersection is essentially the product of the two automata.
$\textbf{Construction 3.2. } \text{Let }L_1\text{ and }L_2\text{ be }\omega\text{-languages recognized by the Büchi automata}\newline\mathcal{A}_1=(\Sigma,Q_1,I_1,T_1,\small\text{BÜCHI}\normalsize(F_1))\text{ and }\mathcal{A}_2 = (\Sigma,Q_2,I_2,T_2,\small\text{BÜCHI}\normalsize (F_2))\text{, respectively.}\newline\text{We construct}\mathcal{A}_\cap=(\Sigma,Q_\cap,I_\cap,T_\cap,\small\text{BÜCHI}\normalsize (F_\cap))\text{ with }\mathcal{L}(\mathcal{A}_\cap)=L_1\cap L_2\text{ as follows:}$
$\begin{array}{rll}
\hspace{1cm} \cdot \ Q_\cap&=&Q_1\times Q_2\times\lbrace 1,2\rbrace\newline
\hspace{1cm} \cdot \ I_\cap&=&I_1\times I_2\times\lbrace 1\rbrace\newline
\hspace{1cm} \cdot \ T_\cap&=&\lbrace (q_1,q_2,i),\sigma ,(q’_1,q’_2,j)\mid (q_1,\sigma,q’_1)\in T_1,(q_2,\sigma,q’_2)\in T_2,i,j\in\lbrace 1,2\rbrace,\newline
\hspace{1cm} \ &&\hspace{5.3cm}q_i \notin F_i\rightarrow i=j \wedge q_i\in F_i\wedge i\neq j\rbrace\newline
\hspace{1cm} \cdot \ F_\cap&=&\lbrace (q_1,q_2,2)\mid q_1\in F_1, q_2\in F_2\rbrace\newline
\end{array}$
| Explaination | |
|---|---|
| $Q_\cap$ | States in the new automaton is tuples that contain the states of two automata plus the third component that used to combine acceptance conditions, e.g. $(q_1,q_2,1)$ is a state. |
| $I_\cap$ | New automaton is constructed with only one initial state, so we assign the value to the acceptance condition {1} for simplicity |
| $T_\cap$ | The switch from $\lbrace 0\rbrace$ and $\lbrace 1\rbrace$ happens nondeterministically. And once you enter the second copy $\lbrace 1\rbrace$, it stays forever. |
| $F_\cap$ | For each transition, it has to be possible by both automata and if such transition reach the one of the automata’s accepting state, the acceptance condition changed. This creates an alternation between the accepting state of the 1st and 2nd automaton. |
Since we start our acceptance condition as {1}, our accepting states of the new automaton will be the accepting states of the 2nd automaton when acceptance condition becomes {2}. i.e. Whenever the run reach to the accepting states of the 2nd automaton, it always has to first reach the accepting states of the 1st automaton.
$\textbf{Theorem 3.3. } \textit{If $L_1$ and $L_2$ are Büchi-recognizable, then so is $L_1\cap L_2$.}$
Formal Proof
The run $r’$ is accepting iff $r_1$ is accepting and $r_2$ is accepting.
i.e. $r’=(q_1^0,q_2^0,t^0)(q_1^1,q_2^1,t^1)\dots$ is a run of $\mathcal{A}_\cap$ on an input word $\alpha$,
iff $r_1 = q^0_1 q^1_1\dots$ is a run of $\mathcal{A}_1$ on $\alpha$ and $r_1 = q^0_2 q^1_2\dots$ is a run of $\mathcal{A}_2$ on $\alpha$
Therefore, an accepting run will be: (1) go to states with {1} → (2) reach accepting state of 1st automaton → (3) go to states with {2} → (4) reach accepting state of 2nd automaton → goes back to (1)…
Next chapter: Closure Properties of the Büchi-recognizable languages (Concatenations)
Further Reading: Closure (mathematics), Intersection (set theory), Union (set theory)
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