PDL with Intersection and Converse is Decidable

C. LutzC. Lutz

Datei:Lutz-CSL-05.ps.gz

Download

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