  We introduce a logic, called LT, to express properties of transductions, i.e.
binary relations from input to output (finite) words. In LT, 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. LT 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, LT has decidable satisfiability and equivalence problems, with tight
non-elementary and elementary complexities, depending on specific
representation of LT-formulas. Our main contribution is a synthesis result:
from any transduction R defined in LT , 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)) belongs to R. As a consequence, we obtain that any
functional transduction is regular iff it is LT-definable. We also investigate
the algorithmic and expressiveness properties of several extensions of LT, and
explicit a correspondence between transductions and data words. As a
side-result, we obtain a new decidable logic for data words.
