{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},
}