Previous chapter: The Muller Acceptance Condition
This is a learning note of a course in CISPA, UdS. Taught by Bernd Finkbeiner
In this section, we want to prove that Muller automata is equivalent to Büchi Automata.
Translate Büchi Automata into Muller Automata
$\textbf{Construction 10.1. } \text{For a (deterministic) Büchi Automaton }\mathcal{A} = (\Sigma,Q,I,T,\small\text{BÜCHI}\normalsize (F))\newline\text{ we define the (deterministic) Muller automaton } \mathcal{A’} = (\Sigma,Q,I,T,\small\text{MULLER} \normalsize (\mathcal{F}))\text{ using}$
$$\mathcal{F}=\lbrace S\subseteq Q\mid S\cap F\neq\varnothing\rbrace$$
Since the construction does not modify the transitions, the Muller automaton is again deterministic if the Büchi automaton is deterministic. It is straightforward to see that the automata recognize the same language.
$\textbf{Theorem 10.1. } \textit{For every (deterministic) Büchi automaton }\mathcal{A}\textit{, there is a (deterministic)}\newline\textit{Muller automaton }\mathcal{A’}\textit{ such that }\mathcal{L(A)}=\mathcal{L(A’)}.$
Proof
The automaton $\mathcal{A’}$ of Construction 10.1 complies with our requirements, according to previous section:
$$\small\text{BÜCHI}\normalsize (F)=\lbrace\alpha\in Q^\omega\mid\text{Inf}(\alpha)\cap F\neq\varnothing\rbrace=\lbrace\alpha\in Q^\omega\mid\text{Inf}(\alpha)\in\mathcal{F}\rbrace=\small\text{MULLER}\normalsize(\mathcal{F})$$
Translate Muller Automata into Büchi Automata
A slightly more difficult construction is to translate the Muller automaton back into a Büchi automaton.
$\textbf{Construction 10.2. } \text{Let }\mathcal{A} = (\Sigma,Q,I,T,\small\text{MULLER} \normalsize (\lbrace F_1,\dots,F_n\rbrace))\text{ be a Muller automaton}\newline\text{and }<\text{ some arbitrary total order on }Q.\text{ We construct the Büchi automaton }\mathcal{A’} = (\Sigma,Q’,\newline I’,T’,\small\text{BÜCHI} \normalsize(F’))\text{ with }\mathcal{A’}\textit{ such that }\mathcal{L(A)}=\mathcal{L(A’)}\text{ as follows:}$
$\begin{array}{llll}
\hspace{1cm} \cdot \ Q’&=Q\cup\overset{n}{\underset{i=1}{\bigcup}}(\lbrace i\rbrace\times F_i\times F_i)\newline
\hspace{1cm} \cdot \ I’&=I\newline
\hspace{1cm} \cdot \ T’&=T\cup\lbrace(q,\sigma,(i,q’,q’))\mid 1\leq i\leq n,(q,\sigma,q’)\in T, q’\in F_i\rbrace\newline
&\hspace{0.9cm}{}\cup\lbrace((i,q,p),\sigma,(i,q’,p’))\mid 1\leq i\leq n,(q,\sigma,q’)\in T,\newline
&\hspace{1.5cm}p’=\left\lbrace\begin{array}{ll} p &\text{if } q\neq p\newline
\text{min}(F_i)&\text{if } q=p=\text{max}(F_i)\newline
\text{min}(F_i\setminus\lbrace r\mid r\leq p\rbrace)&\text{if } q=p<\text{max}(F_i),\end{array}\right.\newline&\hspace{1.5cm}q,p,q’ \in F_i\rbrace\newline
\hspace{1cm} \cdot \ F’&=\overset{n}{\underset{i=1}{\bigcup}}(\lbrace i\rbrace\times \lbrace\text{min}(F_i)\rbrace\times \lbrace\text{min}(F_i)\rbrace)\newline
\end{array}$
Explained in Human language
A run of the Büchi automaton first simply simulates (while in states $Q$) the Muller automaton and then “guesses” the accepting subset of the Muller automaton. The accepting subset is express by the states $(\lbrace i\rbrace\times F_i\times F_i)$, where
- The first component = the index $i$ of the accepting subset,
- The second component = the currently visited state of the Muller automaton, and
- The third component = the “next” state (according to the order on the states) we need to see in order to make progress towards accepting the input word.
The purpose of the order $<$ on the states is that we can “step” through the states of the accepting subset in order to make sure that all states in the accepting subset actually occur infinitely often. In transitions $T’$, we have the transitions
Transitions for all states $Q$ are described by $T$, same as in the original Muller Automaton,
Transitions that contains both states in $Q$ and accepting subset $(\lbrace i\rbrace\times F_i\times F_i)$, it stays in the subset,
Transitions inside the subset,
- the “next” state remain unchanged until the currently visited state visits it $(p=q)$,
- if the currently visited state visits “next” state and it is the last “step” of the subset, it means we visited the entire subset $F_i$ and we should start from the beginning $\text{min}(F_i)$ again.
- otherwise, move one step ahead ($p’ > p$ and $p, p’\in F_i$)
The Büchi automaton accepts if we step through the states of the accepting subset infinitely often.
Recall that we used a similar trick in the construction of the Büchi automaton for the intersection of two Büchi-recognizable languages in Construction 3.2.
$\textbf{Theorem 10.2. } \newline\textit{For every Muller automaton }\mathcal{A}\textit{ there is a Büchi automaton }\mathcal{A’}\textit{ such that }\mathcal{L(A)}=\mathcal{L(A’)}.$
Proof
$\mathcal{L(A)}\subseteq\mathcal{L(A’)}$ (all word accepted by $\mathcal{L(A)}$ must also be accepted by $\mathcal{L(A’)}$):
Let $\alpha\in\mathcal{L(A)}$ and $r=q_0q_1q_2\dots$ be an accepting run of $\mathcal{A}$ on $\alpha$. As $r$ is accepting, we have that:
$\text{Inf}(r)\in\mathcal{F}$, so $r$ must be in one of the accepting subset, i.e. $\text{Inf}(r)=F_i$ for some $1\leq i\leq n$,
Let $m$ be the first position that visit some accepting state: $q_j\in\text{Inf}(r)$ for all $j\geq m$,
Now consider some run of $\mathcal{A’}$ on $\alpha:\ r’ = q_0q_1\dots q_{m−1}(i, q_m, p_0)(i, q_{m+1}, p_1)(i, q_{m+2}, p_2)\dots$
- it nondeterministically switches to $(i, q_m, p_0)$ at position $m$.
For the sake of contradiction, assume that $r$ is not accepting:
- Then there is a position $k\geq 0$ such that $p_j=p_k$ for all $j\geq k$ ($q$ never moves to $p_k$,“next” state got stuck).
- Then also $q_{m+j}\neq p_j$ for all $j\geq k$. However, this contradicts that $p_k\in F_i$.
(if q can never reach $p_k$, then it is not an accepting state and thus contradicts with the definition of the subset)
$\mathcal{L(A)}\supseteq\mathcal{L(A’)}$ (all word accepted by $\mathcal{L(A’)}$ must also be accepted by $\mathcal{L(A)}$):
Let $\alpha\in\mathcal{L(A’)}$, $r’ = q_0q_1\dots q_{m−1}(i, q_m, p_0)(i, q_{m+1}, p_1)(i, q_{m+2}, p_2)\dots$ be some accepting run of $\mathcal{A’}$ on $\alpha$:
- At some position $m$ it switches to some $(i, q_m, p_0)$, otherwise it would not be accepting.
- By construction, $q_j\in\text{Inf}(r)$ for all $j\geq m$ (it starts staying in the accepting subset), and
- For each $p\in F_i$ there are infinitely many positions $k$ such that $q_k=p_k=p$.
- ($q$ always reach every “next” state infinitely often at some positions)
Thus, we can construct an accepting run $r=q_0q_1q_2\dots$ of $\mathcal{A}$ on $\alpha$ by using every $q$ state in the run $r’$, because every second component in the tuple is accepting, i.e. $\text{Inf}(pr_2(r’))=p_k=F_i$,
Summary
Now we have proved that we can construct an Muller automaton from Büchi automaton and an Büchi automaton from Muller automaton. Therefore they are interchangably equivalent. In the next section, we will prove that deterministic Muller automata are actually closed.
Next chapter: Closure Properties of Muller Automata under Boolean Operations
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