AGV 12.3 -- Complementation of Parity Tree Automata

Notes > UdS AGV

Created At : 2025-02-16 20:12

Count:329 Views :

Introduction
1. Proof

This is a learning note of a course in CISPA, UdS. Taught by Bernd Finkbeiner

Introduction

We now prove that parity tree automata are closed under complementation. As discussed at the beginning of the section, our proof makes heavy use of the determinacy of parity games (with infinite game arenas) established in Theorem 11.3.

$\textbf{Theorem 12.3. } \textit{For every parity tree automaton }\mathcal{A}\textit{ over }\Sigma\textit{ there is a parity tree automaton }\mathcal{A}’\newline\textit{ with }\mathcal{L(A’)}=\mathcal{T}_\Sigma\setminus\mathcal{L(A)}.$

Proof

Let $\mathcal{A}=(\Sigma,Q,q_0,T,\small\text{PARITY} \normalsize(C))$. By Theorem 12.1, a tree $(\mathcal{T},t)$ is accepted by $\mathcal{A}$ iff Player 0 has a winning strategy from position $(\varepsilon,q_0)$ of the acceptance game $\mathcal{G}_{\mathcal{A},t}$.

Since $\mathcal{A}$ is a parity tree automaton, $\mathcal{G}{\mathcal{A},t}$ is a parity game and therefore, by Theorem 11.3, memoryless determined. Hence, $\mathcal{A}$ does not accept some tree $t$ iff Player 1 has a winning memoryless strategy $\sigma$ in $\mathcal{G}{\mathcal{A},t}$ from $(\varepsilon,q_0)$.

The strategy $\sigma:\lbrace 0,1\rbrace^\ast\times T\rightarrow\lbrace 0,1\rbrace^\ast\times Q$ can be represented as a function $\sigma’:\lbrace 0,1\rbrace^\ast\times T\rightarrow\lbrace 0,1\rbrace$

where $\sigma(w,(q,\sigma,q^0,q^1))=(wi,q^i)$ iff $\sigma’(w,(q,\sigma,q^0,q^1))=i$. Yet another representation of the same strategy is $\sigma’:\lbrace 0,1\rbrace^\ast\rightarrow\lbrace T\rightarrow\lbrace 0,1\rbrace\rbrace$,

which can be understood as a labeling of $\mathcal{T}$ with finite “local strategies”. Hence, A does not accept $(\mathcal{T},t)$ iff

there is a $(T\rightarrow\lbrace 0,1\rbrace)$-labeled tree $(\mathcal{T},v)$ such that
for all i0i1i2 . . . ∈ {0, 1}

Next chapter: