PDL with Intersection and Converse is Decidable

C. LutzC. Lutz

Datei:Lutz-LTCS-05-05.ps.gz

Download

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