Logics for word transductions and applications

A finite word transduction is a binary relation of finite words. After an introduction on recent results about word transductions, in particular about logics and automata for word transductions and their connections, the talk introduces a new logic to specify properties of word transductions. This logic will lead us to a new characterization of the robust class of so called regular transductions. Decidability results for model-checking and synthesising transductions are also presented. Finally, a strong connection between transductions and data words (over an infinite alphabet) is given, leading to a new decidable logic for data words.

The duration of the talk is around 45 minutes. Basic notions in automata theory and classical logics (FO, MSO) are assumed.