02. – 05. April 2017, Dagstuhl Seminar 17142

Formal Methods of Transformations


Emmanuel Filiot (Free University of Brussels, BE)
Sebastian Maneth (University of Edinburgh, GB)
Helmut Seidl (TU München, DE)

Auskunft zu diesem Dagstuhl Seminar erteilt

Dagstuhl Service Team


Gemeinsame Dokumente


Transducers were invented in the 1960s as formal models for linguistics and syntax-directed translation in compilers. Today, research on string and tree transducers is an active field with various new applications in databases, document processing, natural language processing, software engineering, and verification. The aim of this Dagstuhl Seminar is to bring together researchers in theory and application of transducers. To make the seminar more focused, we have identified the following six research directions as key topics for the seminar:

Canonical Normal Forms
Recently, new canonical normal forms have been established for various classes of tree and tree-to-string transducers. Such normal forms allow to (i) decide equivalence, (ii) optimize transducers through minimization, and to (iii) prove Myhill-Nerode like theorems which in turn enable Gold-style learning algorithms. For many classes decidability of equivalence is known, but effective normal forms are still missing.

Transducer-Logic Relationships
Exciting new results have been established: both string and tree MSO transducers have been characterized in terms of transducers with registers. First-order definable string translations have been characterized by particular machines, and transducer-logic relationships have been obtained for tree-to-string transducers. Also for "symbolic transducers" over infinite alphabets, new logic relationships exist.

Subclass Definability
A huge success in this area has been the recent proof of decidability of one-way transducers, within the class of two-way transducers. The complexity of this has been settled for a subclass, but remains open in general. Moreover, the extension of this result to tree transducers is a challenging open problem. For transducer with origin information, various definability results have been obtained, e.g., to decide first-order definability of two-way transducers, or to decide top-down tree translations within macro tree translations. No counter part of these results is known yet for origin-less transducers.

New Decidability Results
The HOM problem has recently been proven decidable. The proof uses powerful decidability results about tree automata with particular equality and disequality tests. The combination of such automata with transducers is a largely unexplored area that deserved attention. Moreover, it is still open whether equivalence of attributed and macro tree transducers is decidable. For the (large) subclass of top-down tree-to-string transducers decidability has been proven recently.

Complexity and New Transducer Models
It has been shown that the IO- and OI-hierarchies are context-sensitive, by characterizing them through compositions of macro tree transducers. For the more general "unsafe" versions of these hierarchies, it remains a big open problem whether context-sensitivity can be proven. Only for the case of level two, this has been proven recently. New models have been investigated that are tailored towards streaming, such as "streaming (tree) transducers". It has been shown that over streams with forward references, top-down translations can be realized with bounded memory. Many challenging problems remain open here.

Model-Checking Data-Centric Systems
Model-Checking has been successfully applied to reactive systems, where data processing is not central. It remains open how these results can be extended to systems that rely on data processing, e.g., to string manipulating programs. Thus, we would like to investigate formal models for such programs, and to be able to model-check them.

  Creative Commons BY 3.0 DE
  Emmanuel Filiot, Sebastian Maneth, and Helmut Seidl

Related Dagstuhl Seminar


  • Data Structures / Algorithms / Complexity
  • Semantics / Formal Methods
  • Verification / Logic


  • Automata
  • Transducers
  • Formal methods
  • Trees


Bücher der Teilnehmer 

Buchausstellung im Erdgeschoss der Bibliothek

(nur in der Veranstaltungswoche).


In der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.


Download Übersichtsflyer (PDF).


Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von
Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.