Top-down complementation of automata on finite trees (Q6602316)

The contribution discusses a complementation construction for tree automata that avoids the common approach of (bottom-up) determinization and complementation of the designated states. It can thus be called a top-down complementation construction that is motivated and proved by means of game theory. There is little theoretical benefit to this construction except that it returns a deterministic finite-state automaton in case the input ranked alphabet degenerates to a classical string alphabet (i.e., only unary and nullary symbols) and is closer in spirit to constructions for tree automata on infinite trees. However, the presentation of this new construction is nice, easy to follow, well motivated, and complements the existing constructions. In addition, the proof by means of game theory illustrates the strong connection between tree automata theory and game theory that is well-known from the theory of infinite trees, but potentially unknown to the community that exclusively deals with finite structures.\N\NThe author made every possible effort to make the contribution as readable as possible. He provides ample intuition and motivation. Examples are generously used and connections to other approaches are exhibited. While there is no formal proof in the paper I doubt that any reader of the contribution is unconvinced by the arguments laid out. Overall, I believe that this contribution is suitable for anyone with some mild exposure to tree automata theory, but potentially an interesting (and short) read for even experienced researchers in the area.