https://www.dagstuhl.de/17142

### 02. – 05. April 2017, Dagstuhl Seminar 17142

# Formal Methods of Transformations

## Organisatoren

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

## Dokumente

Dagstuhl Report, Volume 7, Issue 4

Motivationstext

Teilnehmerliste

Gemeinsame Dokumente

Dagstuhl's Impact: Dokumente verfügbar

## Summary

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.

**License**

Creative Commons BY 3.0 Unported license

Emmanuel Filiot, Sebastian Maneth, and Helmut Seidl

## Related Dagstuhl Seminar

- 13192: "Tree Transducers and Formal Methods" (2013)

## Classification

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

## Keywords

- Automata
- Transducers
- Formal methods
- Trees