Synthesis of deterministic top-down tree transducers from automatic tree relations

摘要

We consider the synthesis of deterministic tree transducers from automaton definable specifications, given as binary relations, over finite trees. We consider the case of tree-automatic specifications, meaning the specification is recognizable by a top-down tree automaton that reads the two given trees synchronously in parallel. In this setting we study tree transducers that are allowed to have either delay that remains in a given bound or arbitrary delay. Delay is caused whenever the transducer reads a symbol from the input tree without producing output. For specifications that are deterministic top-down tree-automatic, we provide decision procedures for both bounded and arbitrary delay that yield deterministic top-down tree transducers which realize the specification for input trees that are part of the specification domain, and can behave arbitrarily on trees outside the domain. Similarly to the case of relations over words, we use two-player games as the main technique to obtain our results.