PDL with Intersection and Converse is 2EXP-complete

Stefan GöllerStefan Göller, Markus LohreyMarkus Lohrey, Carsten LutzCarsten Lutz

Download

Stefan Göller, Markus Lohrey, Carsten Lutz
PDL with Intersection and Converse is 2EXP-complete
In Helmut Seidl, eds., Proceedings of the Tenth International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'07), volume 4423 of Lecture Notes in Computer Science, 198-212, 2007. Springer

Details
Bibtex

KurzfassungAbstract
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.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

The final publication is available at Springer.

@inproceedings{ GoeLoLu-07,
  author = {Stefan {G\"oller} and Markus {Lohrey} and Carsten {Lutz}},
  booktitle = {Proceedings of the Tenth International Conference on Foundations of Software Science and Computation Structures ({FoSSaCS'07})},
  editor = {Helmut {Seidl}},
  pages = {198--212},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  title = {{PDL} with Intersection and Converse is {2EXP}-complete},
  volume = {4423},
  year = {2007},
}