From Monadic Second-Order Definable String Transformations to Transducers

Courcelle (1992) proposed the idea of using logic, in particular Monadic second-order logic (MSO), to define graph to graph transformations. Transducers, on the other hand, are executable machine models to define transformations, and are typically studied in the context of string-to-string transformations. Engelfriet and Hoogeboom (2001) studied two-way finite state string-to-string transducers and showed that their expressiveness matches MSO-definable transformations (MSOT). Alur and Cerny (2011) presented streaming transducers-one-way transducers equipped with multiple registers that can store output strings, as an equi-expressive model. Natural generalizations of streaming transducers to string-to-tree (Alur and D´Antoni, 2012) and infinite-string-to-string (Alur, Filiot, and Trivedi, 2012) cases preserve MSO-expressiveness. While earlier reductions from MSOT to streaming transducers used two-way transducers as the intermediate model, we revisit the earlier reductions in a more general, and previously unexplored, setting of infinite-string-to-tree transformations, and provide a direct reduction. Proof techniques used for this new reduction exploit the conceptual tools (composition theorem and finite additive coloring theorem) presented by Shelah (1975) in his alternative proof of Bϋchi´s theorem. Using such streaming string-to-tree transducers we show the decidability of functional equivalence for MSO-definable infinite-string-to-tree transducers.