Anzeige
Erschienen in:
2007 | OriginalPaper | Buchkapitel
PDL with Intersection and Converse Is 2EXP-Complete
verfasst von : Stefan Göller, Markus Lohrey, Carsten Lutz
Erschienen in: Foundations of Software Science and Computational Structures
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. 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
.