Relating word and tree automata (Q2576943)

A Büchi word automaton is \(A=\langle\Sigma,Q,\delta,Q_0,F\rangle\), where \(\Sigma\) is the input alphabet, \(Q\) is a finite set of states, \(\delta:Q\times\Sigma\rightarrow 2^Q\) is a transition function, \(Q_0\subseteq Q\) is the set of initial states and \(F\subseteq Q\) is the set of accepting states. If \(A\) has several initial states or the transition function may specify many possible transmissions for each state and letter, \(A\) is nondeterministic. If \(| Q_0| =1\) and \(\delta\) is such that, for every \(q\in Q\) and \(\sigma\in\Sigma\), we have that \(| \delta(q,\sigma)| \leq 1\), then \(A\) is a deterministic automaton. A Büchi tree automaton is \(U=\langle\Sigma,Q,\delta,Q_0,F\rangle\), where \(\Sigma,Q,\delta,Q_0\) and \(F\) are as in Büchi word automata, and \(\delta:Q\times\Sigma\rightarrow 2^{Q\times Q}\) is a (nondeterministic) transition function. Let \(T\) be the infinite binary tree. A run of \(U\) on an input \(\Sigma\)-labeled tree \(V\) is a \(Q\)-labeled tree \(r\) such that \(r(\varepsilon)\in Q_0\) and for every \(x\in T\) we have that \(\langle r(x,0), r(x,1)\rangle\in \delta(r(x),V(x))\). Given a run \(r\) and a path \(\pi\subset T\), let \[ \inf (r| n) =\{q\in Q: \text{ for infinitely many } x\in\pi,\text{ we have } r(x)= q\}. \] A run \(r\) is accepting iff for each path \(\pi\subset T\) there exists a state in \(F\) that \(r\) visits infinitely often along \(\pi\). Rabin word automata are identical to Büchi word automata, only that the acceptance condition \(F\subseteq 2^{Q\times Q}\) is a set \(\{\langle G_1,B_1\rangle,\dots, \langle G_k,B_k\rangle\}\) of pairs of subsets of \(Q\), and a run \(r\) is accepting iff there is \(1\leq i\leq k\) such that \(\inf (r)\cap G_i \neq \emptyset\). Rabin tree automata are indentical to Büchi tree automata, except that a run is accepting iff for each path \(\pi\subset T\), there is \(1\leq i\leq k\) such that \(\inf (r| n)\cap G_i \neq\emptyset\) and \(\inf (r| n)\cap B_i \neq\emptyset\). For a word language \(L\subseteq \Sigma^\omega\), the derived language of \(L\), denoted by \(L_\Delta\), is the set of all trees all of whose paths are labeled with words in \(L\). It is shown that a word language \(L\) is recognizable by a nondeterministic Büchi word automaton but not recognizable by a deterministic Büchi word automaton iff \(L\) is recognizable by a nondeterministic Rabin tree automaton. Let \(U\) be a Büchi tree automaton that recognizes \(L_\Delta\). The authors construct a deterministic Büchi word automaton \(A\) that recognizes \(L\). For \(U\) with \(n\) states, the automaton \(A\) has almost \(2^{n+1}\) states.