Sciweavers

Share
FOSSACS
2006
Springer

Propositional Dynamic Logic with Recursive Programs

10 years 2 months ago
Propositional Dynamic Logic with Recursive Programs
We extend the propositional dynamic logic PDL of Fischer and Ladner with a restricted kind of recursive programs using the formalism of visibly pushdown automata (Alur, Madhusudan 2004). We show that the satisfiability problem for this extension remains decidable, generalising known decidability results for extensions of PDL by non-regular programs. Our decision procedure establishes a 2-ExpTime upper complexity bound, and we prove a matching lower bound that applies already to rather weak extensions of PDL with non-regular programs. Thus, we also show that such extensions tend to be more complex than standard PDL. Key words: Propositional Dynamic Logic, Visibly Pushdown Automata
Christof Löding, Olivier Serre
Added 22 Aug 2010
Updated 22 Aug 2010
Type Conference
Year 2006
Where FOSSACS
Authors Christof Löding, Olivier Serre
Comments (0)
books