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

DOI10.1016/J.IC.2016.07.013MaRDI QIDQ515670zbMATH OpenOpenAlexFDO

Authors Christof Löding, Sarah Winter

Publication date 16 March 2017

Published in Information and Computation (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1408.5959

zbMATH Keywords

automatic relation decidability tree automaton tree transducer uniformization

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Formal languages and automata (68Q45)

Abstract: We consider the synthesis of deterministic tree transducers from automaton definable specifications, given as binary relations, over finite trees. We consider the case of specifications that are deterministic top-down tree automatic, meaning the specification is recognizable 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 realize the specification for valid input trees. Similar to the case of relations over words, we use two-player games to obtain our results.

Review text

This contribution discusses the problem of extracting a deterministic top-down tree transducer, which computes a function, from an efficiently presented relation such that the function computed by the transducer is a subset of the given relation when restricted to the domain of the relation. This problem is also known as uniformization. Here, the relation is presented by a top-down tree automaton that accepts trees in a particular format that represent tree pairs. Such a tree pair is essentially encoded into a single tree by overlaying the two pairs adding a special empty symbol for positions that only exist in one of the trees. The authors distinguish two modes. Either the top-down tree transducer is required to compute a function that has the same domain as the relation or its outputs can be arbitrary on elements outside of the domain of the relation. The decision procedures for the uniformization problem discussed here assume the second mode in which the tree transducer can behave arbitrarily on inputs outside of the domain of the relation. The problem is first solved for top-down tree transducers with bounded delay, which means that the tree transducer can only use a bounded number of rules in sequence that consume part of the input but do not produce part of the output. The problem is reduced to a safety two-player game which is known to be decidable. For the case of unbounded delay, which is obtained by transducers that erase an input symbol and continue processing a single subtree of the input tree, an additional observation is necessary that shows which relations can be uniformized by such behavior. Finally, it remains to detect instances of this behavior, and then another reduction to a two-player game is presented that yields decidability. If the domain of the computed function needs to coincide with the domain of the relation, then the presented results do not carry over and a decidability result is only provided for a very particular kind of top-down tree transducers. Overall, the paper is very well written, but assumes some background in tree language and tree transducer theory. Pointers to the relevant literature are provided and proofs are presented in full detail, so the contribution should be understandable to any graduate computer science student with some effort.

Recommendations

Cites work

Cited in

(9)

This page was built for publication: Synthesis of deterministic top-down tree transducers from automatic tree relations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q515670)