Properties of Visibly Pushdown Transducers⋆

Abstract. Visibly pushdown transducers (VPTs) form a strict subclass of push-down 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, func-tionality is decidable in PTIME, k-valuedness is in NPTIME and equivalence of (non-deterministic) functional VPTs is EXPTIME-C. Those problems are unde-cidable for PTs. Output words of VPTs are not necessarily well-nested. We iden-tify a general subclass of VPTs that produce well-nested words, which is closed by composition, and for which the type checking problem is decidable.