2026-07-072026-07-07http://salesiana.dossiersoluciones.com/handle/123456789/174776String transductions that are definable in monadic second-order (mso) logic (without the use of parameters) are exactly those realized by deterministic two-way finite state transducers. Nondeterministic mso definable string transductions (i.e., those definable with the use of parameters) correspond to compositions of two nondeterministic two-way finite state transducers that have the finite visit property. Both families of mso definable string transductions are characterized in terms of Hennie machines, i.e., two-way finite state transducers with the finite visit property that are allowed to rewrite their input tape.63 pages, LaTeX2e. Extended abstract presented at 26-th ICALP, 1999Logic in Computer ScienceComputational ComplexityF.4.1; F.4.3; F.1.1text