2-ExpTime lower bounds for Propositional Dynamic Logics with intersection

M. LangeM. Lange, Carsten LutzCarsten Lutz

Datei:LangeLutz-JSL-05.ps.gz

Download

M. Lange, Carsten Lutz
2-ExpTime lower bounds for Propositional Dynamic Logics with intersection
Journal of Symbolic Logic, 70(5):1072-1086, 2005

Details
Bibtex

KurzfassungAbstract
In 1984, Danecki proved that satisfiability in IPDL, i.e., Propositional Dynamic Logic (PDL) extended with an intersection operator on programs, is decidable in deterministic double exponential time. Since then, the exact complexity of IPDL has remained an open problem: the best known lower bound was the ExpTime one stemming from plain PDL until, in 2004, the first author established ExpSpace-hardness. In this paper, we finally close the gap and prove that IPDL is hard for 2-ExpTime, thus 2-ExpTime-complete. We then sharpen our lower bound, showing that it even applies to IPDL without the test operator interpreted on tree structures.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@article{ LangeLutzJSL05,
  author = {M. {Lange} and C. {Lutz}},
  journal = {Journal of Symbolic Logic},
  number = {5},
  pages = {1072--1086},
  title = {2-ExpTime lower bounds for Propositional Dynamic Logics with intersection},
  volume = {70},
  year = {2005},
}