PDL with Intersection and Converse is Decidable

PublikationenPublications

• Nach AutorBy Author
  • Carsten LutzCarsten Lutz
• Nach ForschungsgruppeBy Research Group
  • AutomatentheorieAutomata Theory

Toggle side column

PDL with Intersection and Converse is Decidable

Carsten LutzCarsten Lutz

Datei:Lutz-CSL-05.ps.gz

• Download

Carsten Lutz
PDL with Intersection and Converse is Decidable
Annual Conference of the European Association for Computer Science Logic CSL'05, LNCS, 2005. Springer

• Details
• Bibtex

• KurzfassungAbstract
  In its many guises and variations, propositional dynamic logic (PDL) plays an important role in various areas of computer science such as databases, artificial intelligence, and computer linguistics. One relevant and powerful variation is ICPDL, the extension of PDL with intersection and converse. Although ICPDL has several interesting applications, its computational properties have never been investigated. In this paper, we prove that ICPDL is decidable by developing a translation to the monadic second order logic of infinite trees. Our result has applications in information logic, description logic, and epistemic logic. In particular, we solve a long-standing open problem in information logic. Another virtue of our approach is that it provides a decidability proof that is more transparent than existing ones for PDL with intersection (but without converse).
• Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

The final publication is available at Springer.

@inproceedings{ Lutz-CSL-01,
  author = {C. {Lutz}},
  booktitle = {Annual Conference of the European Association for Computer Science Logic CSL'05},
  publisher = {Springer Verlag},
  series = {LNCS},
  title = {PDL with Intersection and Converse is Decidable},
  year = {2005},
}