Visibly pushdown languages are an interesting subclass of deterministic context-free languages that can model nonregular properties
of interest in program analysis. Such class properly contains typical classes of parenthesized languages such as “parenthesis”,
“bracketed”, “balanced” and “input-driven” languages. It is closed under boolean operations and has decidable decision problems
such as emptiness, inclusion and universality. We study the membership problem for visibly pushdown languages, and show that
it can be solved in time linear in both the size of the input grammar and the length of the input word. The algorithm relies
on a reduction to the reachability problem for game graphs. We also discuss the time complexity of the membership problem
for the class of balanced languages which is the largest among those cited above. Besides the intrinsic theoretical interest,
we further motivate our main result showing an application to the validation of XML documents against Schema and Document
Type Definitions (DTDs).
Keywords Visibly pushdown grammars - Verification - XML
Work partially supported by funds for the research from MIUR 2006, grant “Metodi Formali per la verifica di sistemi chiusi
ed aperti”, Università di Salerno.
A preliminary version of this paper was published in the Proceedings of the 4th International Symposium Automated Technology
for Verification and Analysis (ATVA 2006), Lecture Notes in Computer Science 4218, pp. 96–109, 2006.