Previous chapter: Tree Automata and Acceptance Game
This is a learning note of a course in CISPA, UdS. Taught by Bernd Finkbeiner
Emptiness Game
The acceptance game can also be used to test if the language of a given tree automaton is non-empty. For this purpose, we first translate the given automaton into an automaton with singleton alphabet.
$\textbf{Construction 12.1. } \text{For a given tree automaton }\mathcal{A}\text{ over }\Sigma\text{-labeled trees, we consider the}\newline\text{following tree automaton }\mathcal{A}’\text{ over }\lbrace1\rbrace\text{-labeled trees, such that }\mathcal{L(A)}=\varnothing\text{ iff }\mathcal{L(A’)}=\varnothing:\newline
\begin{array}{l}
\hspace{1cm} \cdot \ Q’=Q \newline
\hspace{1cm} \cdot \ q_0’=q_0\newline
\hspace{1cm} \cdot \ T’=\lbrace(q,1,q’,q’’)\mid(q,\sigma,q’,q’’)\in T,\sigma\in\Sigma\rbrace\newline
\hspace{1cm} \cdot \ Acc’ = Acc
\end{array}$
Because the subtrees of a $\lbrace 1\rbrace$-labeled binary tree are the same from all nodes, we can simplify its acceptance game such that only finitely many positions are needed. We call this game the emptiness game.
$\textbf{Definition 12.5. } \text{Let }\mathcal{A}=(\Sigma,Q,q_0,T,Acc)\text{ be a tree automaton. The }\textit{emptiness game}\text{ of }\mathcal{A}\newline \text{ is the game }\mathcal{G}_{\mathcal{A}}=(\mathcal{A}’,\text{Win}’)\text{ with the finite game arena }\mathcal{A}’=(Q\cup T, Q,T,E)\text{, where}\newline E=\lbrace(q,\tau)\mid\tau=(q,\sigma,q^0,q^1),\tau\in T\rbrace\cup\lbrace(\tau,q’)\mid\tau=(\rule{0.5em}{0.4pt},\sigma,q^0,q^1)\text{ and }(q’=q^0\text{ or }q’=q^1)\rbrace\newline\text{and Win’}=\lbrace q(0)\tau(0)q(1)\tau(1)\dots\mid q(0)q(1)\dots\in Acc,\tau(0)\tau(1)\dots\in T^\omega\rbrace$
$\textbf{Theorem 12.2. } \textit{The language of a tree automaton }\mathcal{A}\textit{ is non-empty iff Player 0 wins the}\newline\textit{emptiness game }\mathcal{G}_{\mathcal{A}}\textit{ from position }q_0.$
Proof
The emptiness game corresponds to the acceptance game of the automaton from Construction 12.1 on the $\lbrace 1\rbrace$-labeled binary tree.
Next chapter: Complementation of Parity Tree Automata
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