Skip to main content
SpringerLink
Log in

The Complexity of Hybrid Logics over Equivalence Relations

  • Published:
Journal of Logic, Language and Information Aims and scope Submit manuscript

Abstract

This paper examines and classifies the computational complexity of model checking and satisfiability for hybrid logics over frames with equivalence relations. The considered languages contain all possible combinations of the downarrow binder, the existential binder, the satisfaction operator, and the global modality, ranging from the minimal hybrid language to very expressive languages. For model checking, we separate polynomial-time solvable from PSPACE-complete cases, and for satisfiability, we exhibit cases complete for NP, PSpace, NExpTime, and even N2ExpTime. Our analysis includes the versions of all these languages without atomic propositions, and also complete frames.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  • Areces, C., Blackburn, P., & Marx, M. (1999). A road-map on complexity for hybrid logics. In Proceedings of the 13th CSL, 1999, volume 1683 of LNCS (pp. 307–321). Springer.

  • Areces C., Blackburn P., Marx M. (2000) The computational complexity of hybrid temporal logics. Logic Journal of the IGPL, 8(5): 653–679

    Article  Google Scholar 

  • Blackburn P., Seligman J. (1995) Hybrid languages. Journal of Logic, Language and Information, 4: 251–272

    Article  Google Scholar 

  • Blackburn, P. & Seligman, J. (1998). What are hybrid languages? In M. Kracht, M. de Rijke, H. Wansing, & M. Zakharyaschev (Eds.), Advances in Modal Logic, volume 1 of CSLI Publications (pp. 41–62). Stanford University.

  • Chlebus B.S. (1986) Domino-tiling games. Journal of Computer and System Sciences, 32(3): 374–392

    Article  Google Scholar 

  • Franceschet M, de Rijke M. (2005) Model checking for hybrid logics (with an application to semistructured data). Journal of Applied Logic, 4(3): 279–304

    Article  Google Scholar 

  • Franceschet, M., de Rijke, M., & Schlingloff, B.-H. (2003). Hybrid logics on linear structures: Expressivity and complexity. In Proceedings of the 10th TIME, 2003 (pp. 166–173). IEEE Computer Society.

  • Goranko V. (1996) Hierarchies of modal and temporal logics with reference pointers. Journal of Logic, Language and Information, 5(1): 1–24

    Article  Google Scholar 

  • Ladner R.E. (1977) The computational complexity of provability in systems of modal propositional logic. SIAM Journal on Computing, 6(3): 467–480

    Article  Google Scholar 

  • Lange, M. (2005). A lower complexity bound for propositional dynamic logic with intersection (Vol. 5, pp. 133–147). King’s College Publications.

  • Mundhenk, M., Schneider, T., Schwentick, T., & Weber, V. (2005). Complexity of hybrid logics over transitive frames. In H. Schlingloff (Ed.), M4M, volume 194 of Informatik-Berichte (pp. 62–78). Humboldt-Universität zu Berlin. The cited version is http://arxiv.org/abs/0806.4130v1atarXiv.or.

  • Papadimitriou, C. H. (1994). Computational complexity. Addison-Wesley.

  • SavelsberghM.vanEmde Boas P. (1984) Bounded tiling, an alternative to satisfiability. In: Wechsung G. (eds) 2nd Frege Conference, volume 20 of Mathematische Forschung.. Akademie Verlag, Berlin, pp 354–363

    Google Scholar 

  • ten Cate, B., & Franceschet, M. (2005). On the complexity of hybrid logics with binders. In Proceedings of the 19th CSL, 2005, volume 3634 of LNCS (pp. 339–354). Springer.

  • Vardi, M., & Stockmeyer, L. (1985). Improved upper and lower bounds for modal logics of programs. In Proceedings of the 17th STOC (pp. 240–251).

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, Friedrich-Schiller-Universität, Jena, Germany

    Martin Mundhenk

  2. School of Computer Science, University of Manchester, Manchester, UK

    Thomas Schneider

Authors
  1. Martin Mundhenk
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Thomas Schneider
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Martin Mundhenk.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Mundhenk, M., Schneider, T. The Complexity of Hybrid Logics over Equivalence Relations. J of Log Lang and Inf 18, 493–514 (2009). https://doi.org/10.1007/s10849-009-9089-6

Download citation

  • Received:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10849-009-9089-6

Keywords

Search

Navigation