PDL with Intersection and Converse Is 2 EXP-Complete

We study the complexity of satisfiability for the expressive extension ICPDL of PDL (Propositional Dynamic Logic), which admits intersection and converse as program operations. Our main result is containment in 2EXP, which improves the previously known non-elementary upper bound and implies 2EXPcompleteness due to an existing lower bound for PDL with intersection. The proof proceeds by showing that every satisfiable ICPDL formula has a model of treewidth at most two and then giving a reduction to the emptiness problem for alternating two-way automata on infinite trees. In this way, we also reprove in an elegant way Danecki’s difficult result that satisfiability for PDL with intersection is in 2EXP.

• Type: Conference
• Year: 2007
• Where: FOSSACS
• Authors: Stefan Göller, Markus Lohrey, Carsten Lutz
• Keywords: Applied Computing, Expressive Extension Icpdl, FOSSACS 2007, Non-elementary Upper Bound, Propositional Dynamic Logic