Subject
Equivalence of Tree Transducers
Location
The position is open in the LINKS project-team at INRIA
Lille.
Supervisors
Aurélien Lemay (Université de Lille, INRIA, Links),Sylvain Salvati (Université de Lille, INRIA, Links).
Duration
INRIA is financing 12 to 16 months of postdoc. The postdoc could be extended up to 24 months using the ANR colis fundings.
Start date
During the year 2018.
Special condition
The PhD thesis of the candidate should have been defended either in 2017 or in 2018.
Context
This Post-doc project takes place within the ANR project Colis. Its goal is to certify properties of Linux installation scripts. Our partner of University Paris Diderot models the actions of theses scripts as transformations of file systems viewed as data trees. Then the automatic verification of installation scripts can be obtained using algorithms that manipulate such transformations. Many of the properties that need to be verified can be reduced to the problem of equivalence of those tree transformations. For instance, does the composition of an install script and its uninstall counterpart leave the file system unchanged? We view these tree transformations as tree transducers of various sorts and thus the overall objective is to develop algorithms to solve the equivalence problem of tree transducers efficiently.
Mission
The objective of this project is to define normalisation techniques for models of tree transducers equivalent to Monadic Second Order (MSO) logic. Similar techniques have been developped by members of the Links projects on models such as deterministic top-down tree transducers [LMN10], or Tree to String Transducers [LLN+11, BP16]. Both those models have a sequential behavior. Sequentiality enables normal forms based on the notion of ’earliest’ 1production which is already present in the work of [Cho03] on word transducers. However, these classes are not expressive enough to capture the whole class of MSO tree transformations. The class of Macro Tree Transducers (MTT) captures MSO transformations [EM99], but this models seems to lack the sequentiality properties necessary to apply the same technics.
We propose to investigate other alternate models equivalent to MTT for which the notion of earliestness could be defined. These models would then serve as means to obtain normal forms. In turn this would lead to efficient equivalence algorithms for the whole class of MSO tree transformations. It is expected that, beside its immediate impact on the Colis project, this normal form could also give rise to learning technics that are able to infer transducers from the observation of their behaviors.
Expected Profile
The candidate is expected to have a good competence in formal models, with a focus on models for tree transformations.
References
[BP16] Adrien Boiret and Raphaela Palenta. Deciding equivalence of linear tree-to-word transducers in polynomial time. In Developments in Language Theory – 20th International Conference, DLT 2016, Montréqal, Canada, July 25-28, 2016, Proceedings, pages 355–367, 2016.
[Cho03] Christian Choffrut. Minimizing subsequential transducers: a survey. Theor. Comput. Sci., 292(1):131–143, 2003.
[EM99] Joost Engelfriet and Sebastian Maneth. Macro tree transducers, attribute grammars, and MSO definable tree translations. Inf. Comput., 154(1):34–91, 1999.
[LLN+11] Grégoire Laurence, Aurélien Lemay, Joachim Niehren, Slawek Staworko, and Marc Tommasi. Normalization of sequential top-down tree-to-word transducers. In Language and Automata Theory and Applications – 5th International Conference, LATA 2011, Tarragona, Spain, May 26-31, 2011. Proceedings, pages 354–365, 2011.
[LMN10] Aurélien Lemay, Sebastian Maneth, and Joachim Niehren. A learning algorithm for top-down XML transformations. In Proceedings of the Twenty-Ninth ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, PODS 2010, June 6-11, 2010, Indianapolis, Indiana, USA, pages 285–296, 2010.
