Top-down complementation of automata on finite trees
Laurent Doyen · Information Processing Letters · 2024
We present a new complementation construction for nondeterministic automata on finite trees. The traditional complementation involves determinization of the corresponding bottom-up automaton (recall that top-down deterministic automata are less powerful than nondeterministic automata, whereas bottom-up deterministic automata are equally powerful). The construction works directly in a top-down fashion, therefore without determinization. The main advantages of this construction are: ( i ) in the special case of finite words it boils down to the standard subset construction (which is not the case of the traditional bottom-up complementation construction), and ( i i ) it illustrates the core argument of the complementation lemma for infinite trees, central in the proof of Rabin's tree theorem, in a simpler setting where issues related to acceptance conditions over infinite words and determinacy of infinite games are not present.