AGV 12.2 -- Emptiness Game
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
AGV 12.2 -- Emptiness Game