Logics for Transductions

Logics over words such as Monadic Second-Order Logic, or Linear Temporal Logic provide a way to specify properties of systems in a high-level formalism, close to natural language. From such formulas one would like to decide properties such as satisfiability, model-checking or synthesis problems, and the tight links between logics and automata have provided effective procedures to do so. We present several attempts to generalize some well-known results from languages to transductions (i.e. functions from words to words).