Visibly pushdown languages

TLDR

The authors introduce visibly pushdown languages, a tractable extension of context‑free languages that models program‑analysis questions, and extend the framework to infinite words while preserving closure properties and characterizations. Visibly pushdown languages are defined by tying stack operations to input symbols, making the stack depth deterministic at each position; the authors extend this definition to infinite words while maintaining closure properties and logical characterizations. The resulting VPL class is closed under union, intersection, complementation, renaming, concatenation, Kleene‑*, has Exptime‑complete inclusion, unifies numerous program‑analysis decision procedures, supports verification of recursive programs, and is robustly characterized both logically and via regular tree languages, while for infinite words nondeterministic Büchi visibly pushdown automata are strictly more expressive than deterministic Muller visibly pushdown automata.

Abstract

We propose the class of visibly pushdown languages as embeddings of context-free languages that is rich enough to model program analysis questions and yet is tractable and robust like the class of regular languages. In our definition, the input symbol determines when the pushdown automaton can push or pop, and thus the stack depth at every position. We show that the resulting class Vpl of languages is closed under union, intersection, complementation, renaming, concatenation, and Kleene-*, and problems such as inclusion that are undecidable for context-free languages are Exptime-complete for visibly pushdown automata. Our framework explains, unifies, and generalizes many of the decision procedures in the program analysis literature, and allows algorithmic verification of recursive programs with respect to many context-free properties including access control properties via stack inspection and correctness of procedures with respect to pre and post conditions. We demonstrate that the class Vpl is robust by giving two alternative characterizations: a logical characterization using the monadic second order (MSO) theory over words augmented with a binary matching predicate, and a correspondence to regular tree languages. We also consider visibly pushdown languages of infinite words and show that the closure properties, MSO-characterization and the characterization in terms of regular trees carry over. The main difference with respect to the case of finite words turns out to be determinizability: nondeterministic Büchi visibly pushdown automata are strictly more expressive than deterministic Muller visibly pushdown automata.