A note on an extension of PDL

Recently visibly pushdown automata have been extended to so called k-phase multistack visibly pushdown automata (k-MVPAs). On the occasion of introducing kMVPAs, it has been asked whether the extension of Propositional Dynamic Logic with k-MVPAs still leads to a decidable logic. This question is answered negatively here. Key words: Propositional Dynamic Logic, Visibly Pushdown Automata, Multi-Stack Visibly Pushdown Automata, Decidability, Satisfiability

• Type: Journal
• Year: 2008
• Where: JAPLL
• Authors: Stefan Göller, Dirk Nowotka
• Keywords: JAPLL 2008, K-phase Multistack, Propositional Dynamic Logic, Pushdown