Visibly pushdown automata (VPA) are a natural model for the control
flow of recursive programs and have tight connections with tree
automata and XML schemas. They were considered for parsing
algorithms [1]} under the name “input-driven pushdown
automata”, and shown to have better space complexity than
unrestricted pushdown automata. The name “visibly pushdown automata”
is due to Alur and Madhusudan [2]}, who initiated
their study from the perspective of program verification, and
developed the theory in several directions
(see http://madhu.cs.illinois.edu/vpa/ for an exhaustive list of
results). In particular, they
showed that the class of visibly pushdown languages
shares many desirable properties with the class of regular languages,
like determinization, closure under boolean operations and the
existence of a Myhill-Nerode congruence that defines canonical
VPA [3]}. However, the existence of
a canonical VPA does not help
for minimization, in contrast to regular languages. Similarly
to many other more complex automata models, like automata over infinite words,
two-way automata, etc,
VPA do not have unique minimal automata. Even worse, the canonical VPA can be
exponentially larger than a minimal VPA. Therefore, the minimization
problem for VPA, besides being very relevant in practice, is also very challenging.
