On a Non-Context-Free Extension of PDL
| dc.creator | Göller, Stefan | |
| dc.creator | Nowotka, Dirk | |
| dc.date | 2007-07-04 | |
| dc.date | 2007-07-18 | |
| dc.date.accessioned | 2026-07-07T08:18:40Z | |
| dc.date.available | 2026-07-07T08:18:40Z | |
| dc.description | 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 Σ_1^1-complete. | |
| dc.identifier | https://arxiv.org/abs/0707.0562 | |
| dc.identifier | http://arxiv.org/abs/0707.0562 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/134516 | |
| dc.subject | Logic in Computer Science | |
| dc.title | On a Non-Context-Free Extension of PDL | |
| dc.type | text |