2-ExpTime lower bounds for propositional dynamic logics with intersection
Lange, Martin ; Lutz, Carsten
J. Symbolic Logic, Tome 70 (2005) no. 1, p. 1072-1086 / Harvested from Project Euclid
Text on Project Euclid
PDF
Alt PDF
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.
Publié le : 2005-12-14
Classification:  
@article{1129642115,
     author = {Lange, Martin and Lutz, Carsten},
     title = {2-ExpTime lower bounds for propositional dynamic logics with intersection},
     journal = {J. Symbolic Logic},
     volume = {70},
     number = {1},
     year = {2005},
     pages = { 1072-1086},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1129642115}
}

Lange, Martin; Lutz, Carsten. 2-ExpTime lower bounds for propositional dynamic logics with intersection. J. Symbolic Logic, Tome 70 (2005) no. 1, pp.  1072-1086. http://gdmltest.u-ga.fr/item/1129642115/