Transducersynthese aus automatendefinierbaren Spezifikationen

• Antragsteller: Privatdozent Dr. Christof Löding
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2015 bis 2021
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 287809235

Bei dem Problem der Synthese (oder auch Uniformisierung), soll aus einer Spezifikation vieler möglicher erlaubter Verhaltensweisen eines Systems eine konkrete korrekte Verhaltensweise herausgefiltert und in einem vorgegebenen Formalismus umgesetzt werden. So kann die Spezifikation z.B. mögliche Eingaben zu erlaubten Ausgaben in Beziehung setzen. Sind die Ein- und Ausgaben als Wörter beschrieben, so entspricht die Spezifikation einer Relation über Wörtern. Eine solche Relation kann beispielsweise durch einen endlichen Automaten mit zwei Bändern (für Ein- und Ausgabe) definiert werden. Ziel ist es nun, einen Automaten zu synthetisieren, der zu jeder Eingabe eine konkrete Ausgabe produziert (also eine Funktion berechnet), so dass das Ein-/Ausgabepaar in der Relation enthalten ist. In der Automatentheorie gibt es eine Fülle von Modellen zur Beschreibung von Relationen und Funktionen sowohl über Wörtern als auch Bäumen. Durch die Variation dieser Modelle ergibt sich eine große Anzahl von Syntheseproblemen für unterschiedliche Formalismen zur Beschreibung der Spezifikation sowie zur Implementierung der gewünschten Funktion. In diesem Projekt möchten wir die Entscheidbarkeit sowie ggfs. die genaueren Komplexitäten des Syntheseproblems für die unterschiedlichen automatentheoretischen Formalismen untersuchen.

• DFG-Verfahren: Sachbeihilfen