On a Non-Context-Free Extension of PDL

Details On a Non-Context-Free Extension of PDL On a Non-Context-Free Extension of PDL

2007-07-04

arxiv.org/abs/0707.0562v2

Computer Science

Logic in Computer Science

Scientific paper

Over the last 25 years, a lot of work has been done on seeking for decidable non-regular extensions of Propositional Dynamic Logic (PDL). Only recently, an expressive extension of PDL, allowing visibly pushdown automata (VPAs) as a formalism to describe programs, was introduced and proven to have a satisfiability problem complete for deterministic double exponential time. Lately, the VPA formalism was extended to so called k-phase multi-stack visibly pushdown automata (k-MVPAs). Similarly to VPAs, it has been shown that the language of k-MVPAs have desirable effective closure properties and that the emptiness problem is decidable. On the occasion of introducing k-MVPAs, it has been asked whether the extension of PDL with k-MVPAs still leads to a decidable logic. This question is answered negatively here. We prove that already for the extension of PDL with 2-phase MVPAs with two stacks satisfiability becomes \Sigma_1^1-complete.

Affiliated with

Also associated with

No associations

Rating

On a Non-Context-Free Extension of PDL does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with On a Non-Context-Free Extension of PDL, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and On a Non-Context-Free Extension of PDL will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-547191