Logik
und Theorie
diskreter Systeme

Informatik 7

Transducer Synthesis from Automaton Definable Specifications

Christof Löding, Sarah Winter

The synthesis problem (also referred to as uniformization problem) asks, given a specification that describes many possible allowed behaviors of a system, whether a concrete correct behavior can be filtered out and implemented in a given formalism. For example, a specification can relate possible inputs to allowed outputs. If the inputs and outputs are given as words, then the specification can be viewed as a relation over words. Such relations can be defined, e.g., using finite automata with two tapes (input and output tape). The goal is now to synthesize an automaton that produces for each input a correct output, i.e., an automaton that realizes a function such that each input/output pair is part of the relation. The field of automata theory offers a rich landscape of models for defining relations and functions over both words and trees. Varying these models results in a large number of synthesis problems for different formalisms to describe the specification as well as to implement the desired function. Our aim in this project is to study decidability as well as, if possible, complexity questions of the synthesis problem asked for various automata theoretic models.

Funding: DFG

Publications

  1. Emmanuel Filiot, Ismaël Jecker, Christof Löding and Sarah Winter. On Equivalence and Uniformisation Problems for Finite Transducers. In Proceedings of the 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy. 2016, 125:1–125:14. URL, DOI BibTeX

    @inproceedings{FJLW16,
    	author = {Emmanuel Filiot and Isma{\"{e}}l Jecker and Christof L{\"{o}}ding and Sarah Winter},
    	title = "On Equivalence and Uniformisation Problems for Finite Transducers",
    	booktitle = "Proceedings of the 43rd International Colloquium on Automata, Languages, and Programming, {ICALP} 2016, July 11-15, 2016, Rome, Italy",
    	pages = "125:1--125:14",
    	year = 2016,
    	doi = "10.4230/LIPIcs.ICALP.2016.125",
    	url = "http://arxiv.org/abs/1602.08565"
    }
    
  2. Christof Löding and Sarah Winter. Uniformization Problems for Tree-Automatic Relations and Top-Down Tree Transducers. In Proceedings of the 41st International Symposium on Mathematical Foundations of Computer Science, MFCS 2016, August 22-26, 2016, Kraków, Poland. 2016, 65:1–65:14. DOI BibTeX

    @inproceedings{LW16a,
    	author = {Christof L{\"{o}}ding and Sarah Winter},
    	title = "Uniformization Problems for Tree-Automatic Relations and Top-Down Tree Transducers",
    	booktitle = "Proceedings of the 41st International Symposium on Mathematical Foundations of Computer Science, {MFCS} 2016, August 22-26, 2016, Krak{\'{o}}w, Poland",
    	pages = "65:1--65:14",
    	year = 2016,
    	doi = "10.4230/LIPIcs.MFCS.2016.65"
    }
    
  3. Christof Löding and Sarah Winter. Synthesis of deterministic top-down tree transducers from automatic tree relations. Information and Computation, 2016. DOI BibTeX

    @article{LW16b,
    	author = {Christof L{\"{o}}ding and Sarah Winter},
    	title = "Synthesis of deterministic top-down tree transducers from automatic tree relations",
    	journal = "Information and Computation",
    	year = 2016,
    	doi = "10.1016/j.ic.2016.07.013"
    }