Visibly pushdown automata have been recently introduced by Alur and Madhusudan as a subclass of pushdown automata. This class
enjoys nice properties such as closure under all Boolean operations and the decidability of language inclusion. Along the
same line, we introduce here visibly pushdown transducers as a subclass of pushdown transducers. We study properties of those
transducers and identify subclasses with useful properties like decidability of type checking as well as preservation of regularity
of visibly pushdown languages.
This research was supported by the Belgian FNRS grant 2.4530.02 of the FRFC project “Centre Fédéré en Vérification” and by
the project “MoVES”, an Interuniversity Attraction Poles Programme of the Belgian Federal Government.