The word problem for visibly pushdown languages described by grammars

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). 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.