Survey on transducers of (nested) words: decidability, logic and algebra

Pierre-Alain Reynier
Aix-Marseille University
Friday, 20 May, 2016 - 14:00
Forum H (ULB, La Plaine)
Algorithmic formal verification has proved to be a promising technology to improve reliability and quality of software systems. These works are rooted in the theory of regular languages, that enjoy important automata-logic-algebra connections. In order to address software systems realizing input/output transformations (such as edition, pattern replacement, refactorization…), the model of word-to-word transducers appears as a natural candidate. Fundamental problems concerning transducers include equivalence, type checking, closure under composition, but also determinisation and minimisation. This talk will provide a survey about transducers, and more precisely (if time permits): i) decidability results based on patterns, that allow to derive efficient decision procedures, ii) logic and algebra connections, iii) extensions to nested words.