Synthesis of transducers from relations on finite words and trees

Winter, Sarah; Löding, Christof; Grädel, Erich; Puppis, Gabriele

doi:HT020047185

Synthesis of transducers from relations on finite words and trees = Transducersynthese aus Relationen über endlichen Wörtern und Bäumen

Winter, Sarah^RWTH*

2018 & 2019

Verantwortlichkeitsangabevorgelegt von Sarah Winter, M.Sc.

ImpressumAachen 2018

Umfang1 Online-Ressource (viii, 182 Seiten) : Illustrationen

Dissertation, RWTH Aachen University, 2018

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University 2019

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Löding, Christof (Thesis advisor)^RWTH* ; Grädel, Erich (Thesis advisor)^RWTH* ; Puppis, Gabriele (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2018-12-19

Online
DOI: 10.18154/RWTH-2019-04126
URL: http://publications.rwth-aachen.de/record/760326/files/760326.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
rational relations (frei) ; synthesis (frei) ; transducers (frei) ; tree relations (frei) ; uniformization (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Bei dem Problem der Synthese (beziehungsweise effektiver Uniformisierung), soll aus einer Spezifikation vieler möglicher erlaubter Verhaltensweisen eines Systems eine konkrete korrekte Verhaltensweise herausgefiltert und in einem vorgegebenen Formalismus umgesetzt werden. Wir betrachten die Synthese von Transducern aus automatendefinierbaren Spezifikationen über endlichen Wörtern und Bäumen. In dieser Arbeit führen wir eine neue Variante des folgenden Problems ein: Gegeben eine rationale Relation und eine Klasse von subsequentiellen Transducern, hat die Relation eine Uniformisierung durch einen subsequentiellen Transducer, der in der gegebenen Klasse liegt? Die bisher in der Literatur untersuchten Entscheidungsprobleme behandeln entweder Uniformisierung durch synchrone oder durch beliebige subsequentielle Transducer. Wir untersuchen die folgende Variante: Gegeben eine rationale Relation, hat die Relation eine Uniformisierung durch einen subsequentiellen Transducer indem das erlaubte Ein- und Ausgabeverhalten durch eine Synchonisationssprache definiert ist? Wir zeigen Entscheidbarkeits- und Unentscheitbarkeitsresultate für verschiedene Kombinationen von rationalen, automatischen, und erkennbaren Relationen und Klassen von Synchonisationssprachen. Im Hinblick auf Synthese aus baumautomatischen Spezifikationen zeigen wir, dass es unentscheidbar ist, ob eine solche Relation durch einen deterministischen top-down Baumtransducer uniformisiert werden kann. Wir identifizieren zwei Fälle für die Entscheidbarkeit gilt. Wenn wir uns einschränken auf pfadtreue Transducer (diese sind spezielle lineare Transducer), dann wird das Problem entscheidbar. Wenn wir Relationen betrachten, die durch eine endliche Vereinigung von top-down-deterministischen baumautomatischen Relationen definiert sind, dann wird das Syntheseproblem entscheidbar für synchrone Transducer (diese produzieren genau ein Ausgabesymbol in einem Schritt jedoch können sie non-linear sein). Bei der Untersuchung von Entscheidungsproblemen für Transducer ist es oft ein Hindernis das Transducer die gleiche Transformation auf sehr unterschiedliche Weisen erreichen können. Eine Möglichkeit, um das Studium dieser Probleme einfacher zu gestalten, ist das Entwickeln von Ähnlichkeitsmaßen zwischen Transducern. Dies erlaubt es uns über ähnliche Transducer zu reden. Wir entwickeln für top-down Baumtransducer zwei Ähnlichkeitsmaße und untersuchen, ob ein gegebener top-down Baumtransducer eine Uniformisierung durch einen deterministischen top-down Baumtransducer hat, der ähnlich arbeitet. Wir zeigen für jedes beliebe erlaubte Maß an Unähnlichkeit, dass das Problem entscheidbar ist für Spezifikationen die durch top-down Baumtransducer ohne epsilon-Transitionen gegeben sind.

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.

OpenAccess:
PDF
(additional files)