April 2 – 5 , 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)

For support, please contact

Dagstuhl Service Team


Dagstuhl Report, Volume 7, Issue 4 Dagstuhl Report
List of Participants
Shared Documents


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

Book exhibition

Books from the participants of the current Seminar 

Book exhibition in the library, ground floor, during the seminar week.


In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.


Download overview leaflet (PDF).


Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.

NSF young researcher support