On the Complexity of Hybrid Logics with Binders

  • Balder ten Cate
  • Massimo Franceschet
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3634)


Hybrid logic refers to a group of logics lying between modal and first-order logic in which one can refer to individual states of the Kripke structure. In particular, the hybrid logic HL(@, ↓ ) is an appealing extension of modal logic that allows one to refer to a state by means of the given names and to dynamically create new names for a state.

Unfortunately, as for the richer first-order logic, satisfiability for the hybrid logic HL(@, ↓ ) is undecidable and model checking for HL(@, ↓ ) is PSpace-complete. We carefully analyze these results and we isolate large fragments of HL(@, ↓ ) for which satisfiability is decidable and model checking is below PSpace.


Model Check Modal Logic Kripke Structure Hybrid Logic Model Check Problem 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Andréka, H., van Benthem, J., Németi, I.: Modal logics and bounded fragments of predicate logic. Journal of Philosophical Logic 27, 217–274 (1998)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Grädel, E.: On the restraining power of guards. Journal of Symbolic Logic 64, 1719–1742 (1999)zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    Mortimer, M.: On languages with two variables. Zeitschrift für mathematische Logik und Grundlagen der Mathematik 21, 135–140 (1975)zbMATHMathSciNetCrossRefGoogle Scholar
  4. 4.
    Grädel, E., Otto, M.: On logics with two variables. Theoretical computer science 224, 73–113 (1999)zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Areces, C., Blackburn, P., Marx, M.: Hybrid logics: Characterization, interpolation, and complexity. Journal of Symbolic Logic 66, 977–1010 (2001)zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    ten Cate, B.: Interpolation for extended modal languages. Journal of Symbolic Logic 70, 223–234 (2005)zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    ten Cate, B.: Model theory for extended modal languages. PhD thesis, University of Amsterdam, ILLC Dissertation Series DS-2005-01 (2005)Google Scholar
  8. 8.
    Franceschet, M., de Rijke, M.: Model checking for hybrid logics (with an application to semistructured data). Journal of Applied Logics (2005) (to appear)Google Scholar
  9. 9.
    Blackburn, P., Seligman, J.: Hybrid languages. Journal of Logic, Language and Information 4, 251–272 (1995)zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    Harel, D.: Recurring dominoes: making the highly undecidable highly understandable. Annals of Discrete Mathematics 24, 51–72 (1985)zbMATHMathSciNetGoogle Scholar
  11. 11.
    Goranko, V.: Hierarchies of modal and temporal logics with reference pointers. Journal of Logic, Language, and Information 5, 1–24 (1996)zbMATHCrossRefMathSciNetGoogle Scholar
  12. 12.
    Areces, C., Blackburn, P., Marx, M.: A road-map on complexity for hybrid logics. In: Flum, J., Guez-Artalejo, M.R. (eds.) Proceedings of the 8th Annual Conference of the EACSL, Madrid (1999)Google Scholar
  13. 13.
    Marx, M.: Narcissists, stepmothers and spies. In: Proceedings of the International Workshop on Description Logics (2002)Google Scholar
  14. 14.
    Fisher, M., Ladner, R.: Propositional dynamic logic of regular programs. Journal of Computer and System Sciences 18, 194–211 (1979)CrossRefMathSciNetGoogle Scholar
  15. 15.
    Areces, C., Blackburn, P., Marx, M.: The computational complexity of hybrid temporal logics. Logic Journal of the IGPL 8, 653–679 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  16. 16.
    ten Cate, B., Franceschet, M.: Guarded fragments with constants. Journal of Logic, Language, and Information (2005) (to appear)Google Scholar
  17. 17.
    Börger, E., Grädel, E., Gurevich, Y.: The Classical Decision Problem. Springer, Berlin (1997)zbMATHGoogle Scholar
  18. 18.
    ten Cate, B., Franceschet, M.: On the complexity of hybrid logics with binders. Technical Report PP-2005-02, ILLC, University of Amsterdam (2005)Google Scholar
  19. 19.
    Vardi, M.Y.: On the complexity of bounded-variable queries. In: Proceedings of the ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, pp. 266–276 (1995)Google Scholar
  20. 20.
    ten Cate, B., Franceschet, M.: Guarded fragments with constants. Technical Report PP-2004-32, ILLC, University of Amsterdam (2004)Google Scholar
  21. 21.
    Blackburn, P.: Representation, reasoning, and relational structures: A hybrid logic manifesto. Logic Journal of the IGPL 8, 339–365 (2000)zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Balder ten Cate
    • 1
  • Massimo Franceschet
    • 1
    • 2
  1. 1.Informatics InstituteUniversity of AmsterdamAmsterdamThe Netherlands
  2. 2.Department of SciencesUniversity “G. D’Annunzio”PescaraItaly

Personalised recommendations