From Monadic Second-Order Definable String Transformations to Transducers
Rajeev Alur, Antoine Durand-Gasselin, and Ashutosh Trivedi
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--oneway 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 Buechi's theorem.
Using such streaming string-to-tree transducers we show the decidability of functional equivalence
for MSO-definable infinite-string-to-tree transducers.
Proceedings of the 28th Annual Symposium on Logic in Computer Science (LICS), IEEE Computer Society Press, 2013.
PDF © 2013 IEEE.