Synthesis of Deterministic Top-Down Tree Transducers from Tree-Automatic Specifications

In this talk, we consider the synthesis of deterministic tree transducers from automaton definable specifications, given as binary relations, over finite trees.

In the first part, we focus on the case of specifications that are deterministic top-down tree automatic, meaning the specification is recognisable by a deterministic 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 bounded delay or arbitrary delay.  Delay is caused whenever the transducer reads a symbol from the input tree but does not produce output.  We provide decision procedures for both bounded and arbitrary delay that yield deterministic top-down tree transducers which realise the specification for valid input trees.  Technically, these results are achieved by using two-player games.

In the second part, we will look at the synthesis of deterministic top-down tree transducers from general non-deterministic tree-automatic specifications.  We address the challenges of the synthesis problem in this case and propose different approaches to tackle this problem.  This is joint work with Christof Loeding.

Speaker biography

Sarah Winter is a PhD student in the Group of Logic and Theory of Discrete Systems at RWTH Aachen University under the supervision of Christof Loeding.  She received her bachelors degree in Computer Science in 2011 and her masters degree in Computer Science in 2014 (both from RWTH Aachen University).  Her research activities focus on synthesis of tree transducers.