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 [R. Alur, P. Madhusudan, Visibly pushdown languages, in: Procceings of the 36th Annual ACM Symposium on Theory of Computing (STOC 2004), 2004, ACM, pp. 202–211]. 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.