Synthesis of transducers from relations on finite words and trees

• Transducersynthese aus Relationen über endlichen Wörtern und Bäumen

Winter, Sarah; Löding, Christof (Thesis advisor); Grädel, Erich (Thesis advisor); Puppis, Gabriele (Thesis advisor)

Aachen (2018, 2019)
Dissertation / PhD Thesis

Dissertation, RWTH Aachen University, 2018

Abstract

A uniformization of a binary relation is a function that is contained in the relation and has the same domain as the relation. The synthesis problem asks for effective uniformization for classes of relations and functions that can be implemented in a specific way. We consider the synthesis of transducers from automaton definable specifications on finite words and trees. In this thesis we introduce a new variant of the following decision problem: Given a rational relation on finite words and a class of subsequential transducers, does the given relation have a uniformization by a subsequential transducer from the given class? The decision problems that have been studied previously in the literature either ask for uniformization by a synchronous subsequential or by an arbitrary subsequential transducer. We investigate the following variant: Given a rational relation on finite words, does the given relation have a uniformization by a subsequential transducer in which the allowed input/output behavior is specified by a given language of synchronizations? We exhibit decidability and undecidability results for different combinations of classes of rational relations (precisely for rational, automatic and recognizable relations) and classes of synchronization languages. Regarding synthesis from tree-automatic specifications, we show that it is undecidable whether such a relation has a uniformization by a deterministic top-down tree transducer. On the positive side, we identify two cases for which the problem remains decidable. If we restrict the transducers to be path-preserving, which is a subclass of linear transducers, then the synthesis problem is decidable for general tree-automatic relations. If we consider relations that are finite unions of deterministic top-down tree-automatic relations, then the problem is decidable for synchronous transducers, which produce exactly one output symbol in each step (but can be non-linear).A hindrance in the study of decision problems for transducers is often that transducers are able to accomplish the same transformation but in very different ways. In other words, their behavior is very different. A way to make the study of these problems more feasible is to introduce similarity measures between transducers in order to be able to talk about transducers that behave in a somewhat similar fashion. For top-down tree transducers, we develop two similarity measures and study the following problem: Given a top-down tree transducer, does there exist a similar deterministic top-down tree transducer that realizes the specification defined by the given top-down tree transducer? For any given bound on the dissimilarity (in terms of our similarity measure) between the specification and the implementation, we show decidability of this problem for specifications given by top-down tree transducers without epsilon-transitions.