Abstract
Visibly pushdown transducers (VPTs) form a strict subclass of pushdown transducers (PTs) that extends finite state transducers with a stack. Like visibly pushdown automata, the input symbols determine the stack operations. It has been shown that visibly pushdown languages form a robust subclass of context-free languages. Along the same line, we show that word transductions defined by VPTs enjoy strong properties, in contrast to PTs. In particular, functionality is decidable in PTime, k-valuedness is in NPTime and equivalence of (non-deterministic) functional VPTs is ExpTime-c. Those problems are undecidable for PTs. Output words of VPTs are not necessarily well-nested. We identify a general subclass of VPTs that produce well-nested words, which is closed by composition, and for which the type checking problem is decidable.
Work supported by the projects: (i) QUASIMODO (FP7- ICT-STREP-214755), (ii) GASICS (ESF-EUROCORES LogiCCC), (iii) Moves: “Fundamental Issues in Modelling, Verification and Evolution of Software”, http://moves.ulb.ac.be, a PAI program funded by the Federal Belgian Gouvernment, and (iv) ECSPER (ANR-JC09-472677) and SFINCS (ANR-07-SESU-012), two projects supported by the French National Research Agency.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alur, R.: Marrying words and trees. In: PODS. LNCS, vol. 5140, pp. 233–242. Springer, Heidelberg (2007)
Alur, R., Madhusudan, P.: Visibly pushdown languages. In: STOC, pp. 202–211 (2004)
Béal, M.-P., Carton, O., Prieur, C., Sakarovitch, J.: Squaring transducers: an efficient procedure for deciding functionality and sequentiality. TCS 292(1), 45–63 (2003)
Blattner, M., Head, T.: Single-valued a-transducers. JCSS 15(3), 310–327 (1977)
Comon, H., Dauchet, M., Gilleron, R., Löding, C., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications (2007), http://www.grappa.univ-lille3.fr/tata
Engelfriet, J., Maneth, S.: Macro tree translations of linear size increase are MSO definable. SICOMP 32, 950–1006 (2003)
Engelfriet, J., Maneth, S.: The equivalence problem for deterministic MSO tree transducers is decidable. IPL 100(5), 206–212 (2006)
Engelfriet, J., Vogler, H.: Macro tree transducers. JCSS 31(1), 71–146 (1985)
Filiot, E., Raskin, J.-F., Reynier, P.-A., Servais, F., Talbot, J.-M.: On functionality of visibly pushdown transducers. CoRR, abs/1002.1443 (2010)
Gurari, E.M., Ibarra, O.H.: A note on finite-valued and finitely ambiguous transducers. MST 16 (1983)
Harju, T., Ibarra, O.H., Karhumaki, J., Salomaa, A.: Some decision problems concerning semilinearity and commutation. JCSS 65 (2002)
Ibarra, O.H.: Reversal-bounded multicounter machines and their decision problems. JACM 25(1), 116–133 (1978)
Inaba, K., Maneth, S.: The complexity of translation membership for macro tree transducers. CoRR, abs/0910.2315 (2009)
Koch, C., Scherzinger, S.: Attribute grammars for scalable query processing on XML streams. VLDB 16(3), 317–342 (2007)
Maneth, S., Neven, F.: Structured document transformations based on XSL. In: Connor, R.C.H., Mendelzon, A.O. (eds.) DBPL 1999. LNCS, vol. 1949, pp. 80–98. Springer, Heidelberg (2000)
Perst, T., Seidl, H.: Macro forest transducers. IPL 89(3), 141–149 (2004)
Plandowski, W.: Testing equivalence of morphisms on context-free languages. In: van Leeuwen, J. (ed.) ESA 1994. LNCS, vol. 855, pp. 460–470. Springer, Heidelberg (1994)
Raskin, J.-F., Servais, F.: Visibly pushdown transducers. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part II. LNCS, vol. 5126, pp. 386–397. Springer, Heidelberg (2008)
Schützenberger, M.P.: Sur les relations rationnelles. In: Automata Theory and Formal Languages. LNCS, vol. 33, pp. 209–213. Springer, Heidelberg (1975)
Seidl, H.: Single-valuedness of tree transducers is decidable in polynomial time. TCS 106(1), 135–181 (1992)
Seidl, H.: Equivalence of finite-valued tree transducers is decidable. MST 27(4), 285–346 (1994)
Sénizergues, G.: T(A) = T(B)? In: Wiedermann, J., Van Emde Boas, P., Nielsen, M. (eds.) ICALP 1999. LNCS, vol. 1644, pp. 665–675. Springer, Heidelberg (1999)
Staworko, S., Laurence, G., Lemay, A., Niehren, J.: Equivalence of deterministic nested word to word transducers. In: Gȩbala, M. (ed.) FCT 2009. LNCS, vol. 5699, pp. 310–322. Springer, Heidelberg (2009)
Verma, K.N., Seidl, H., Schwentick, T.: On the complexity of equational horn clauses. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 337–352. Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Filiot, E., Raskin, JF., Reynier, PA., Servais, F., Talbot, JM. (2010). Properties of Visibly Pushdown Transducers. In: Hliněný, P., Kučera, A. (eds) Mathematical Foundations of Computer Science 2010. MFCS 2010. Lecture Notes in Computer Science, vol 6281. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15155-2_32
Download citation
DOI: https://doi.org/10.1007/978-3-642-15155-2_32
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15154-5
Online ISBN: 978-3-642-15155-2
eBook Packages: Computer ScienceComputer Science (R0)