Logics for Word Transductions with Synthesis.

We introduce a logic, called L-T, to express properties of transductions, i.e. binary relations from input to output (finite) words. In L-T, the input/output dependencies are modelled via an origin function which associates to any position of the output word, the input position from which it originates. L-T is well-suited to express relations (which are not necessarily functional), and can express all regular functional transductions, i.e. transductions definable for instance by deterministic two-way transducers. Despite its high expressive power, L-T has decidable satisfiability and equivalence problems, with tight non-elementary and elementary complexities, depending on specific representation of L-T-formulas. Our main contribution is a synthesis result: from any transduction R defined in L-T, it is possible to synthesise a regular functional transduction f such that for all input words u in the domain of R, f is defined and (u, f (u)). R. As a consequence, we obtain that any functional transduction is regular iff it is L-T-definable. We also investigate the algorithmic and expressiveness properties of several extensions of L-T, and explicit a correspondence between transductions and data words. As a side-result, we obtain a new decidable logic for data words.