Information Technology Reference
In-Depth Information
that define functions whose output tree size depends linearly on the size of
the input tree. It is shown in [22,8] that functional MSOT-transformations of
ranked trees are definable by macro tree transducers. The other, more dicult
direction, which shows that macro tree transducers of linear-size increase are
effectively MSOT-definable was proved in [23]. A consequence of this effective
correspondence is the decidability of equivalence for linear-size increase macro
tree transducers. It was indeed shown in [24] that MSO-transducers of ranked
trees have decidable equivalence problem (see [33] for a survey on equivalence
problems for tree transducers).
Other connections between MSO-transducers and tree transducers have been
obtained, for an extension of streaming string transducers to trees [4], and for
some classes of tree walking transducers [15].
Acknowledgments.
I warmly thank Jean-Francois Raskin and Jean-Marc Tal-
bot for reading preliminary versions of this paper, and Sebastian Maneth for his
helpful comments.
References
1. Alur, A., Cerny, P.: Streaming transducers for algorithmic verification of single-
pass list-processing programs. In: POPL, pp. 599-610 (2011)
2. Alur, R., Cerny, P.: Expressiveness of streaming string transducers. In: FSTTCS,
vol. 8, pp. 1-12 (2010)
3. Alur, R., Filiot, E., Trivedi, A.: Regular transformations of infinite strings. Tech-
nical Report MS-CIS-12-05, University of Pennsylvania (2012)
4. Alur, R., D'Antoni, L.: Streaming tree transducers. In: Czumaj, A., Mehlhorn,
K., Pitts, A., Wattenhofer, R. (eds.) ICALP 2012, Part II. LNCS, vol. 7392, pp.
42-53. Springer, Heidelberg (2012)
5. Alur, R., Deshmukh, J.V.: Nondeterministic streaming string transducers. In:
Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011, Part II. LNCS, vol. 6756,
pp. 1-20. Springer, Heidelberg (2011)
6. Alur, R., Durand-Gasselin, A., Trivedi, A.: From monadic second-order definable
string transformations to transducers. In: LICS, pp. 458-467 (2013)
7. Beal, M.-P., Carton, O., Prieur, C., Sakarovitch, J.: Squaring transducers: an e-
cient procedure for deciding functionality and sequentiality. Theoretical Computer
Science 292(1), 45-63 (2003)
8. Bloem, R., Engelfriet, J.: A comparison of tree transductions defined by monadic
second order logic and by attribute grammars. J. Comput. Syst. Sci. 61(1), 1-50
(2000)
9. Bojanczyk, M.: Transducers with origin information. In: Esparza, J., Fraigniaud,
P., Husfeldt, T., Koutsoupias, E. (eds.) ICALP 2014, Part II. LNCS, vol. 8573,
pp. 26-37. Springer, Heidelberg (2014)
10. Buchi, J.R.: Weak second-order arithmetic and finite automata. Zeitschrift fur
Mathematische Logik und Grundlagen der Mathematik 6(1-6), 66-92 (1960)
11. Buchi, J.R.: On a decision method in restricted second-order arithmetic. In: Int.
Congr. for Logic Methodology and Philosophy of Science, pp. 1-11. Standford
University Press, Stanford (1962)
