2-ExpTime lower bounds for Propositional Dynamic Logics with intersection

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche

Toggle side column

2-ExpTime lower bounds for Propositional Dynamic Logics with intersection

M. LangeM. Lange,  Carsten LutzCarsten Lutz
M. Lange, Carsten Lutz
2-ExpTime lower bounds for Propositional Dynamic Logics with intersection
Journal of Symbolic Logic, 70(5):1072-1086, 2005
  • 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},
}