Dagstuhl Seminar 13192
Tree Transducers and Formal Methods
( May 05 – May 08, 2013 )
(Click in the middle of the image to enlarge)
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/13192
Organizers
- Sebastian Maneth (NICTA, AU & University of New South Wales - Sydney, AU)
- Helmut Seidl (TU München, DE)
Contact
- Andreas Dolzmann (for scientific matters)
- Annette Beyer (for administrative matters)
The aim of this Dagstuhl Seminar is to bring together researchers from various research areas related to the theory and application of tree transducers. Tree transducers are a classical formalism in computer science, dating back to the early days of compilers and syntax-directed translation. Recently, interest in tree transducers has been revived due to surprising new applications in areas such as XML databases, security verification, programming language theory, and linguistics. This seminar therefore aims to inspire the exchange of theoretical results and information regarding the practical requirements related to tree transducers. Both fundamental and applied research directions will be considered.
Topics of interests are:
- Expressiveness versus Complexity - Which transducers offer the best trade-offs between expressiveness and complexity?
- Implementability under resource restrictions - Which transducer models can be executed by devices with bounded resources, e.g., for processing XML streams?
- New Applications - What new challenges do the different application areas of tree transducers raise? What new solutions have been found?
- Open Problems - Which are the most pressing open problems in tree transducer theory?
We plan to discuss these topics in three types of sessions: overview, small group, and summary. In the first, participants receive an overview of the state-of-the-art and open research issues within the contributing research areas. In the second, they discuss more focused specific topics in small groups. In the third, they address and summarize the results of small group discussions.
We are convinced that the seminar will provide a unique chance to interchange new ideas related to tree transducers, to distinguish between solved and open questions in the field, and to initiate new collaborations.
The Dagstuhl seminar 13192 "Tree Transducers and Formal Methods" was a short two and a half day seminar that took place from May 5th to 8th, 2013. The aim was to bring together researchers from various research areas related to the theory and application of tree transducers. Tree transducers are a classical formalism in computer science, dating back to the early days of compilers and syntax-directed translation. Recently, interest in tree transducers has been revived due to surprising new applications in areas such as XML databases, security verification, programming languages, and linguistics. This seminar was meant to inspire the exchange of theoretical results and practical requirements related to tree transducers. These points were addressed in particular:
- Expressiveness versus Complexity: Which transducers offer the best trade-offs between expressiveness and complexity?
- Implementability under Resource Restrictions: Which transducer models can be executed by devices with bounded resources, e.g., for processing XML streams?
- New Applications: What new challenges do the different application areas of tree transducers raise? What new solutions have been found?
- Open Problems: Which are the most pressing open problems in tree transducer theory?
The seminar fully satisfied our expectations. The 33 participants from 13 countries (Australia, Belgium, Canada, Czech, France, Germany, Great Britain, Hungary, Japan, Poland, Slovakia, Sweden, and the US) had been invited by the organizer Sebastian Maneth to give particular survey talks about their recent research on applications and theory of tree transducers. There were talks focusing on very practical issues such as Margus Veanes' talk on software verification using symbolic tree transducers (which kicked off the meeting), and also talks on highly challenging theoretical results such as the talk by Emmanuel Filiot on their recent breakthrough of proving that one-wayness of a two-way word automaton is decidable. The other application areas, besides verification, were (1) tree processing (related to databases and search) (2) learning, and (3) linguistics.
The first talk by Veanes on symbolic transducers was followed by Jan Janousek about using pushdown automata to search for tree patterns, in linear order of trees. Symbolic transducers, from a theoretical point of view, were discussed in Heiko Vogler's talk in the afternoon. Input driven pushdown automata, also known as nested word automata or visibly pushdown automata, were discussed with respect to descriptional complexity by Kai Salomaa. The second morning session of the first day was devoted to MSO translations, first about its theory with respect to word and tree translations by Bruno Courcelle, and then concerning a one-pass and linear time implementation model for MSO tree translations: the streaming tree transducer by Loris d'Antoni. The first afternoon section was about higher-order transducers, recursion schemes, and verification, given by Kazuhiro Inaba, Luke Ong, and Naoki Kobayashi. They discussed the open problem of proving context-sensitivity of the unsafe OI-hierarchy, results on model checking of higher-order recursion schemes, and practical approaches to type checking unsafe higher-order tree transducers.
The second day started with theoretical results about word and tree transducers by Emmanuel Filiot and Sebastian Maneth. The latter one was about deciding two database notions, namely determinacy and rewriting, for top--down and MSO tree transducers. Next was a sequence of talks about streaming, by Joachim Niehren, Pavel Labath, and Keisuke Nakano. They discussed practical aspects of early query answering, streaming of macro tree transducers using parallel streams, and stack attributed tree transducers, respectively. Related to streaming was the following talk by Frederic Servais which surveyed recent results on visibly pushdown transducers. The following three talks discussed learning algorithms: first about tree series by Johanna Björklund and Frank Drewes, and then about top--down tree transformations by Adrien Boiret. The last talk of the second day was Florent Jacquemard and Sophie Tison's survey about tree automata with constraints.
The final day started with a talk about natural language processing using transducers, given by Daniel Gildea. It presented applications of multi bottom-up tree transducers to machine translation of natural language. It was followed by a talk by Uwe Mönnich on logical definitions of mildly context-sensitive grammar formalisms. A survey on "the tree-based approach" to natural language grammars was given by Marco Kuhlmann. Damian Niwinski's talk connected to the session of the first day on higher-order schemes: they are equivalent to panic automata, the invention and topic of Damian. An important practical consideration is incremental evaluation: it was discussed for XPath by Henrik Björklund and for succinct regular expressions by Wim Martens.
We thank Schloss Dagstuhl for the professional and inspiring atmosphere it provides. Such an intense research seminar is possible because Dagstuhl so perfectly meets all researchers' needs. For instance, elaborate research discussions in the evening were followed by musical intermezzi of playing piano trios by Beethoven and Mozart, or by table tennis matches and sauna sessions.
Creative Commons BY 3.0 Unported license
Sebastian Maneth and Helmut Seidl
- Henrik Björklund (University of Umeå, SE) [dblp]
- Johanna Björklund (University of Umeå, SE) [dblp]
- Adrien Boiret (ENS - Paris, FR) [dblp]
- Bruno Courcelle (University of Bordeaux, FR) [dblp]
- Loris d'Antoni (University of Pennsylvania - Philadelphia, US) [dblp]
- Frank Drewes (University of Umeå, SE) [dblp]
- Emmanuel Filiot (Université Paris-Est Créteil, FR) [dblp]
- Zoltan Fülöp (University of Szeged, HU) [dblp]
- Olivier Gauwin (University of Bordeaux, FR) [dblp]
- Daniel Gildea (University of Rochester, US) [dblp]
- Kazuhiro Inaba (Google Japan, JP) [dblp]
- Florent Jacquemard (IRCAM & INRIA - Paris, FR) [dblp]
- Jan Janousek (Czech Technical University - Prague, CZ) [dblp]
- Naoki Kobayashi (University of Tokyo, JP) [dblp]
- Marco Kuhlmann (Uppsala University, SE) [dblp]
- Pavel Labath (Comenius University in Bratislava, SK) [dblp]
- Aurélien Lemay (University of Lille III, FR) [dblp]
- Sebastian Maneth (NICTA, AU & University of New South Wales - Sydney, AU) [dblp]
- Wim Martens (Universität Bayreuth, DE) [dblp]
- Uwe Mönnich (Universität Tübingen, DE) [dblp]
- Keisuke Nakano (The University of Electro-Communications - Tokyo, JP) [dblp]
- Joachim Niehren (INRIA - University of Lille 1, FR) [dblp]
- Damian Niwinski (University of Warsaw, PL) [dblp]
- Chih-Hao Luke Ong (University of Oxford, GB) [dblp]
- Pierre-Alain Reynier (University of Marseille, FR) [dblp]
- Kai T. Salomaa (Queen's University - Kingston, CA) [dblp]
- Helmut Seidl (TU München, DE) [dblp]
- Frédéric Servais (Hasselt University - Diepenbeek, BE) [dblp]
- Jean-Marc Talbot (Aix-Marseille University, FR) [dblp]
- Sophie Tison (Lille I University, FR) [dblp]
- Jan Van den Bussche (Hasselt University - Diepenbeek, BE) [dblp]
- Margus Veanes (Microsoft Corporation - Redmond, US) [dblp]
- Heiko Vogler (TU Dresden, DE) [dblp]
Related Seminars
Classification
- programming languages / compiler
- semantics / formal methods
- verification / logic
Keywords
- formal methods
- tree transducers
