Synthesis of transducers from automaton definable specifications

给定系统可能允许的行为规范，合成（或均匀化）的目标是自动构造满足规范的具体系统，并以给定的形式实现。规范可以，例如，将可能的输入与可接受的输出联系起来。如果输入和输出被编码为词，那么规范是词上的关系。这样的关系可以被定义，例如，通过一个有两个磁带的有限自动机（用于输入和输出）。在这种情况下，合成的目标是构造一个自动机，为每个输入计算一个输出（从而计算一个函数），使得输入-输出对处于关系中。在自动机理论中，有许多模型用于描述词和树上的关系和功能。这就产生了许多合成问题的不同formalsims用于描述规范和实现的功能。在这个项目中，我们要分析不同的自动机理论形式化的综合问题的可判定性和复杂性。

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.