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)
Doktorarbeit

Dissertation, RWTH Aachen University, 2018

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.