02. – 05. April 2017, Dagstuhl Seminar 17142
Formal Methods of Transformations
Auskunft zu diesem Dagstuhl Seminar erteilen
Simone Schilke zu administrativen Fragen
Marc Herbstritt zu wissenschaftlichen Fragen
(Zum Einloggen bitte Seminarnummer und Zugangscode verwenden)
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.
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.
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 and Sebastian Maneth and Helmut Seidl
Related Dagstuhl Seminar
- 13192: "Tree Transducers and Formal Methods" (2013)
- Data Structures / Algorithms / Complexity
- Semantics / Formal Methods
- Verification / Logic
- Formal methods