2007 | OriginalPaper | Chapter
PDL with Intersection and Converse Is 2EXP-Complete
Authors : Stefan Göller, Markus Lohrey, Carsten Lutz
Published in: Foundations of Software Science and Computational Structures
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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 2
EXP
, which improves the previously known non-elementary upper bound and implies 2
EXP
-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 2
EXP
.