PDL with Intersection and Converse is Decidable

Carsten Lutz
PDL with Intersection and Converse is Decidable
Technical Report, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, volume LTCS-05-05, 2005. LTCS-Report

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. However, 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).
Bemerkung: Note: See http://lat.inf.tu-dresden.de/research/reports.html.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@techreport{ Lutz-LTCS-05-05,
  address = {Germany},
  author = {C. {Lutz}},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-05-05},
  title = {PDL with Intersection and Converse is Decidable},
  type = {LTCS-Report},
  year = {2005},
}

PDL with Intersection and Converse is Decidable

PDL with Intersection and Converse is Decidable

Carsten LutzCarsten Lutz