Synthesis of transducers from automaton definable specifications

点击翻译按钮获取中文摘要

Given a specification of possible allowed behaviors of a system, the goal of synthesis (or uniformisation) is to automatically construct a concrete system that satisfies the specification, and is implemented in a given formalism. The specification can, e.g., relate possbile inputs to admissible outputs. If the inputs and outputs are coded as words, then the specification is a relation over words. Such a relation can be defined, e.g., by a finite automaton with two tapes (for input and output). In this setting, the goal of synthesis is to construct an automaton that computes one output for each input (and thus computes a function), such that the input-output pairs are in the relation. In automata theory there are many models for describing relations and functions over words and trees. This gives rise to many synthesis problems for the different formalsims used for describing the specification and the implementation of the function. In this project we want to analyze the decidability and the complexities of the synthesis problem for different automata theoretic formalisms.