2-ExpTime lower bounds for Propositional Dynamic Logics with intersection

M. LangeM. Lange, C. LutzC. Lutz

Datei:LangeLutz-JSL-05.ps.gz

Download

M. Lange, C. 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},
}