|
On the Expressive Power of 2-Stack Visibly Pushdown Automata Benedikt Bollig LSV, ENS de Cachan, France. 15-02-08 Abstract Visibly pushdown automata, which have been introduced by Alur and Madhusudan in 2004, are input-driven pushdown automata that recognize some non-regular context-free languages while preserving the nice closure and decidability properties of finite automata. Visibly pushdown automata with multiple s tacks have been considered recently by La Torre, Madhusudan, and Parlato, who exploit the concept of visibility further to obtain a rich pushdown-automata class that can even recognize properties beyond the class of context-free languages. At the same time, their automata are closed under boolean operations, come with a decidable emptiness and inclusion problem, and enjoy a logical characterization in terms of monadic second-order logic over nested words, which add a nesting structure to ordinary words. These results require a restricted version of visibly pushdown automata: The domain is restricted to words whose behavior can be split up into a fixed number of pop phases. In this talk, we consider 2-stack visibly pushdown automata (i.e., visibly pushdown automata with two stacks) in their unrestricted form. We establish that 2-stack visibly pushdown automata are expressively equivalent to the existential fragment of monadic second-order logic. Furthermore, over nested words, monadic second-order quantifier alternation forms an infinite hierarchy (unlike in the restricted domain of La Torre et al., where full monadic second-order logic is only as expressive as its existential fragment). We can therefore conclude that 2-stack visibly pushdown automata are not closed under complementation. Finally, we discuss the expressive power of Buchi 2-stack visibly pushdown automata running over infinite words. Extending the logic by an infinity quantifier, we can likewise establish equivalence to existential monadic second-order logic.
|
