Abstract
We study the complexity of satisfiability in 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 2EXP-completeness due to an existing lower bound for PDL with intersection. The proof proceeds by showing that every satisfiable ICPDL formula has a model of tree-width at most two and then giving a reduction to the (non)-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. © Springer-Verlag Berlin Heidelberg 2007.
Cite
CITATION STYLE
Göller, S., Lohrey, M., & Lutz, C. (2007). PDL with intersection and converse Is 2EXP-complete. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4423 LNCS, pp. 198–212). Springer Verlag. https://doi.org/10.1007/978-3-540-71389-0_15
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
