In addition, we refer to [1]}, [2]}, [3]} for background on visibly pushdown automata and visibly pushdown languages (\(\operatorname{VPLang}\) ) but also give here the main definitions. More precisely, a pushdown alphabet \(\widetilde{\Sigma }\)  is a triple \((\Sigma _c, \Sigma _i, \Sigma _r)\)  of pairwise-disjoint alphabets known as the call, internal and return alphabets respectively. A visibly pushdown automaton (VPA) is a pushdown automaton for which the stack operations (i.e. whether a push, pop or neither is performed) are determined by the input symbol which is read. In particular, any transition for which the input symbol \(a\)  belongs to the call alphabet \(\Sigma _c\) , must push a symbol to the stack while any transition for which \(a \in \Sigma _r\)  must pop a symbol from the stack unless the stack is empty and any transition for which \(a \in \Sigma _i\)  must leave the stack unchanged. Acceptance of a word is determined by the state the automaton is in after reading the whole word. The stack does not need to be empty for a word to be accepted. A \(\widetilde{\Sigma }\) -visibly pushdown language is the set of words accepted by a visibly pushdown automaton with pushdown alphabet \(\widetilde{\Sigma }\) . A language \(L\)  is a visibly pushdown language (and is part of the class \(\operatorname{VPLang}\) ) if there exists a pushdown alphabet \(\widetilde{\Sigma }\)  such that \(L\)  is a \(\widetilde{\Sigma }\) -visibly pushdown language. The class \(\operatorname{VPLang}\)  is a strict superset of the class of regular languages and a strict subset of the class of deterministic context-free languages, which retains many of the nice decidability and closure properties of regular languages. In particular, it is shown in [1]} that \(\operatorname{VPLang}\)  is closed under union, intersection and complement and moreover that the emptiness, universality, inclusion and equivalence probelms are all decidable for \(\operatorname{VPLang}\) .
