Logic in Computer Science, Symposium on (2013)

New Orleans, LA, USA USA

June 25, 2013 to June 28, 2013

ISSN: 1043-6871

ISBN: 978-1-4799-0413-6

pp: 458-467

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2013.52

ABSTRACT

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 'ern' (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.

INDEX TERMS

Registers, Transducers, Computational modeling, Cost accounting, Context, Additives, Automata, tree transducers, Streaming string transducers, monadic second-order logic, $\omega$-regular transformations

CITATION

Rajeev Alur,
Antoine Durand-Gasselin,
Ashutosh Trivedi,
"From Monadic Second-Order Definable String Transformations to Transducers",

*Logic in Computer Science, Symposium on*, vol. 00, no. , pp. 458-467, 2013, doi:10.1109/LICS.2013.52