Dagstuhl Seminar 17142
Formal Methods of Transformations
( Apr 02 – Apr 05, 2017 )
(Click in the middle of the image to enlarge)
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/17142
Organizers
- Emmanuel Filiot (Free University of Brussels, BE)
- Sebastian Maneth (University of Edinburgh, GB)
- Helmut Seidl (TU München, DE)
Contact
- Simone Schilke (for administrative matters)
Impacts
- Composition Closure of Linear Extended Top-down Tree Transducers : article - Engelfriet, Joost; Fülöp, Zoltan; Maletti, Andreas - Berlin : Springer, 2017. - pp. 129-171 - (Theory of computing systems ; 60. 2017 : article).
- Multiple context-free tree grammars: Lexicalization and characterization : article - Engelfriet, Joost; Maletti, Andreas; Maneth, Sebastian - Amsterdam : Elsevier, 2018. - pp. 29-99 - (Theoretical computer science ; 728. 2018).
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
The Dagstuhl seminar 17142 ``Formal Methods of Transformations'' was a short two and half day seminar that took place from April 3rd to 5th, 2017. The aim of this seminar was to bring together researchers working on theory and applications of formal models of transformations (also known as transductions) of strings and trees. A model of transformation which has been central in this seminar is that of a transducer, i.e., an automaton extended with output. Transducers were introduced 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. To make the seminar more focused, we had identified six research directions as key topics for the seminar:
- Canonical Normal Forms: it is well-known that regular languages admit a unique minimal (and canonical) deterministic finite automaton. Similarly, is it possible to characterize classes of transformations by canonical normal form for transducers?
- Transducer-Logic Relationships: there are well-known automata-logic correspondences in the theory of languages. What is known for transformations and can we obtain similar connections?
- Subclass Definability: a fundamental question, which requires a deep understanding of the manipulated objects, is that of subclass definability: given (an effective description of) an object in some class $C$, does this object belong to a given subclass $C'$ of $C$? What are the recent results and open problems with respect to subclass definability for transformations?
- New Decidability Results: what are the recent decidability breakthroughs in the theory of transformations and what are the important open problems?
- New Transducer Models: is there a need for new transducer models tailored to new applications?
- Model-Checking Data-Centric Systems: what are the potential applications of transducer theory to the verification of systems that transform data?
The seminar gave a large overview of recent results and open problems with respect to these research directions. It was a follow-up of Dagstuhl seminar 13192 "Tree Transducers and Formal Methods", which now included researchers on string transducers. String transducers have indeed received a lot of attention in the recent years and new important results have been obtained. The aim of this seminar was also to gather researchers from the string and tree transducer communities. There were 31 participants from 10 countries (Sweden, France, Poland, Germany, US, Belgium, UK, Japan, Portugal, and India). These participants were invited by the organizers Emmanuel Filiot, Sebastian Maneth, and Helmut Seidl to give survey talks and shorter talks on their current research.
The seminar started with a survey talk by Emmanuel Filiot on recent results on string transformations, intended to motivate the need to address the theory of string transformations in this seminar, and to introduce some of its main recent breakthroughs. Mikolaj Bojanczyk then gave a survey talk on the notion of origins in transformations. Origins are inherent to all known transducer models and making them explicit in the semantics of transducers gave rise to new decidability and definability results. Mikolaj's talk was followed by a session on string transducers. Luc Dartois presented a new and expressive logic to define string transformations. The logic offers good decidability properties with respect to satisfiability and equivalence (under the origin semantics). String transformations, under the origin semantics, can be seen as sets of graphs, called origin graphs. Bruno Guillon presented a characterization of the class of origin graphs generated by known string transducer models. Finally, Jacques Sakarovitch closed this session by presenting a contribution, and an open problem, on rational base numeration systems and their analysis by means of automata and transducers.
The afternoon session started with a survey talk by Christof Löding on the automatic synthesis of deterministic transducers of strings and trees, from specifications given by non-deterministic transducers. This problem, called the uniformization problem, can be seen as a variant of the classical Church synthesis problem. Two short talks given by Nathan Lhote and Michaël Cadilhac presented their recent contributions on definability problems for string transducers. Nathan Lhote presented decidability results for checking whether a given rational function is first-order definable, and, more generally, whether it is definable by some string transducer whose (input) transition monoid (which disregards the outputs) belongs to some given class, thus lifting to transformations well-known results from the theory of regular languages. Michaël Cadilhac then introduced the notion of C-continuity for string transformations and showed effectiveness of this notion for particular classes C. This notion gives an alternative and machine-independent way, which also takes outputs into account, of defining meaningful subclasses of transformations.
Day 2 (morning) was a session devoted to applications. It started with a survey talk on symbolic transducers, by Margus Veanes. Symbolic transducers have been introduced to address practical issues when dealing with very large alphabets (even infinite). Transition labels are replaced by predicates defining sets of allowed labels. Fundamental decidability results and practical applications were presented. Based on symbolic string transducers, Loris d'Antoni then presented a fully automatic method to invert a practical class of functional (and injective) transformations, implemented in the tool GENIC. Adrien Boiret then addressed the problem of checking equivalence for symbolic top-down tree transducers. Keisuke Nakano presented some fundamental results on B-terms, which model function composition. Finally, the morning session ended with a talk by Olivier Carton about the notion of infinite word compression by transducers and its relation to normality.
Andreas Maletti started the afternoon session with a survey talk on tree transducers and their applications in linguistics. He presented transducer models well-suited to some linguistic applications such as automatic natural language translation, and showed a comparison with deep learning approaches. Frank Drewes then discussed the notion of graph transformations, and especially of DAGs, and proposed in his talk a definition of DAG transducers. Motivated by natural-language interface applications, Johanna Björklund presented a study of the expressivity of checking stack transducers, which extend with outputs the well-known model of checking stack automata. Day 2 ended with a talk by Helmut Seidl on a result obtained together with Sebastian Maneth and Gregor Kemper on the decidability of equivalence for deterministic top-down tree-to-string transducers, which had been a long standing open problem.
The last day was dedicated to results on the class of string transformations defined by two-way transducers, mostly definability problems. There were two talks, one by Olivier Gauwin and one by Jean-Marc Talbot, presenting two different techniques, for deciding whether a transformation in this class can be defined by a one-way transducers, i.e., is rational. It was open whether this problem was solvable in elementary time, and the two presented approaches answer this question positively. Another definability problem about the minimization of the number of registers in subclasses of SSTs (a model introduced by Alur and Cerny, with the same expressivity as two-way transducers), was discussed by Pierre-Alain Reynier. Ismaël Jecker presented a class of transducers with strong constraints on their structures, but still as expressive as too-way transducers, and at the same time enjoying many good algorithmic properties, in particular improving by one exponential a famous result by Hopcroft and Ullman. Finally, Krishna S. concluded the seminar by sketching an alternative proof of a result by Alur et. al. on regular expressions for string transformations.
We had long after-lunch breaks (till 4pm) to give the opportunity to the participants to discuss. It was greatly appreciated by the participants, and some of them initiated new collaborations. The discussions inspired new ideas and we hope that joint papers will be published by the participants.
We warmly thank Schloss Dagstuhl for making this fruitful event possible, and for their help in the organization. It is highly appreciated as organizers, and allowed us to focus only on the scientific aspects of the seminar.
Emmanuel Filiot, Sebastian Maneth, and Helmut Seidl
- Johanna Björklund (University of Umeå, SE) [dblp]
- Adrien Boiret (INRIA Lille, FR) [dblp]
- Mikolaj Bojanczyk (University of Warsaw, PL) [dblp]
- Michaël Cadilhac (Universität Tübingen, DE) [dblp]
- Olivier Carton (University Paris-Diderot, FR) [dblp]
- Loris d'Antoni (University of Wisconsin - Madison, US) [dblp]
- Luc Dartois (Free University of Brussels, BE) [dblp]
- Frank Drewes (University of Umeå, SE) [dblp]
- Emmanuel Filiot (Free University of Brussels, BE) [dblp]
- Olivier Gauwin (University of Bordeaux, FR) [dblp]
- Bruno Guillon (University of Warsaw, PL) [dblp]
- Florent Jacquemard (IRCAM & INRIA - Paris, FR) [dblp]
- Ismaël Jecker (Free University of Brussels, BE) [dblp]
- Shankaranarayanan Krishna (Indian Institute of Technology - Mumbai, IN) [dblp]
- Aurélien Lemay (INRIA Lille, FR) [dblp]
- Nathan Lhote (University of Bordeaux, FR) [dblp]
- Christof Löding (RWTH Aachen, DE) [dblp]
- Andreas Maletti (Universität Leipzig, DE) [dblp]
- Sebastian Maneth (University of Edinburgh, GB) [dblp]
- Anca Muscholl (University of Bordeaux, FR) [dblp]
- Keisuke Nakano (The University of Electro-Communications - Tokyo, JP) [dblp]
- Joachim Niehren (INRIA Lille, FR) [dblp]
- Chih-Hao Luke Ong (University of Oxford, GB) [dblp]
- Raphaela Palenta (TU München, DE) [dblp]
- Rogério Reis (University of Porto, PT) [dblp]
- Pierre-Alain Reynier (Aix-Marseille University, FR) [dblp]
- Jacques Sakarovitch (Telecom ParisTech, FR) [dblp]
- Helmut Seidl (TU München, DE) [dblp]
- Frédéric Servais (Free University of Brussels, BE) [dblp]
- Jean-Marc Talbot (Aix-Marseille University, FR) [dblp]
- Margus Veanes (Microsoft Corporation - Redmond, US) [dblp]
Related Seminars
Classification
- data structures / algorithms / complexity
- semantics / formal methods
- verification / logic
Keywords
- automata
- transducers
- formal methods
- trees
