PDL with Intersection and Converse Is Decidable

  • Carsten Lutz
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3634)


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).


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Afanasiev, L., Blackburn, P., Dimitriou, I., Gaiffe, B., Goris, E., Marx, M., de Rijke, M.: PDL for ordered trees. Journal of Applied Non-Classical Logic (2005) (to appear)Google Scholar
  2. 2.
    Alechina, N., Demri, S., de Rijke, M.: A modal perspective on path constraints. Journal of Logic and Computation 13(6), 939–956 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    Baader, F.: Augmenting concept languages by transitive closure of roles: An alternative to terminological cycles. In: Proc. of IJCAI 1991, Sydney, Australia, pp. 446–451 (1991)Google Scholar
  4. 4.
    Balbiani, P., Vakarelov, D.: Iteration-free PDL with intersection: a complete axiomatization. Fundamenta Informaticae 45, 1–22 (2001)MathSciNetGoogle Scholar
  5. 5.
    Berardi, D., Calvanese, D., De Giacomo, G., Lenzerini, M., Mecella, M.: Automatic composition of e-services that export their behavior. In: Orlowska, M.E., Weerawarana, S., Papazoglou, M.P., Yang, J. (eds.) ICSOC 2003. LNCS, vol. 2910, pp. 43–58. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  6. 6.
    Calvanese, D., De Giacomo, G., Lenzerini, M.: On the decidability of query containment under constraints. In: Proc. of PODS 1998, pp. 149–158 (1998)Google Scholar
  7. 7.
    Danecki, R.: Nondeterministic propositional dynamic logic with intersection is decidable. In: Skowron, A. (ed.) SCT 1984. LNCS, vol. 208, pp. 34–53. Springer, Heidelberg (1985)Google Scholar
  8. 8.
    De Giacomo, G., Lenzerini, M.: PDL-based framework for reasoning about actions. In: Proc. of AI*IA 1995, vol. 992, pp. 103–114. Springer, Heidelberg (1995)Google Scholar
  9. 9.
    Donini, F.M., Lenzerini, M., Nardi, D., Nutt, W.: The complexity of concept languages. Information and Computation 134(1), 1–58 (1997)zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press, Cambridge (1995)zbMATHGoogle Scholar
  11. 11.
    Farinas Del Cerro, L., Orlowska, E.: DAL-a logic for data analysis. Theoretical Computer Science 36(2-3), 251–264 (1985)zbMATHCrossRefMathSciNetGoogle Scholar
  12. 12.
    Fischer, M.J., Ladner, R.E.: Propositional modal logic of programs. In: Conference record of the ninth annual ACM Symposium on Theory of Computing, pp. 286–294. ACM Press, New York (1977)CrossRefGoogle Scholar
  13. 13.
    Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18, 194–211 (1979)zbMATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    Giacomo, G.D., Lenzerini, M.: Boosting the correspondence between description logics and propositional dynamic logics. In: Proc. of AAAI 1994, vol. 1, pp. 205–212. AAAI Press, Menlo Park (1994)Google Scholar
  15. 15.
    Harel, D.: Dynamic logic. In: Handbook of Philosophical Logic, vol. II, pp. 496–604. D. Reidel Publishers, Dordrecht (1984)Google Scholar
  16. 16.
    Kozen, D.: Results on the propositional μ-calculus. In Automata, Languages and Programming. In: Nielsen, M., Schmidt, E.M. (eds.) ICALP 1982. LNCS, vol. 140, pp. 348–359. Springer, Heidelberg (1982)CrossRefGoogle Scholar
  17. 17.
    Lange, M.: A lower complexity bound for propositional dynamic logic with intersection. In: Advances in Modal Logic, vol. 5, King’s College Publications (2005)Google Scholar
  18. 18.
    Lange, M., Lutz, C.: 2-ExpTime lower bounds for propositional dynamic logics with intersection (2005) (submitted)Google Scholar
  19. 19.
    Lutz, C.: PDL with intersection and converse is decidable. LTCS-Report 05-05, Technical University Dresden (2005), Available from
  20. 20.
    Lutz, C., Sattler, U.: Mary likes all cats. In: Proc. of DL 2000. CEUR-WS, vol. 33, pp. 213–226 (2000),
  21. 21.
    Massacci, F.: Decision procedures for expressive description logics with role intersection, composition and converse. In: Proc. of IJCAI 2001, San Francisco, CA, August 4-10, pp. 193–198. Morgan Kaufmann Publishers, Inc., San Francisco (2001)Google Scholar
  22. 22.
    Pratt, V.: Considerations on floyd-hoare logic. In: FOCS: IEEE Symposium on Foundations of Computer Science, FOCS (1976)Google Scholar
  23. 23.
    Schild, K.D.: A correspondence theory for terminological logics: Preliminary report. In: Proc. of IJCAI 1991, pp. 466–471. Morgan Kaufmann, San Francisco (1991)Google Scholar
  24. 24.
    Vardi, M.Y., Wolper, P.: Automata-theoretic techniques for modal logic of programs. Journal of Computer and System Sciences 32, 183–221 (1986)zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Carsten Lutz
    • 1
  1. 1.Institute for Theoretical Computer ScienceTU DresdenGermany

Personalised recommendations