The complexity of hybrid logics over equivalence relations

Martin Mundhenk, Thomas Schneider

    Research output: Contribution to journalArticlepeer-review

    37 Downloads (Pure)


    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. © Springer Science+Business Media B.V. 2009.
    Original languageEnglish
    Pages (from-to)493-514
    Number of pages21
    JournalJournal of Logic, Language and Information
    Issue number4
    Publication statusPublished - Sept 2009


    • Downarrow operator
    • Hybrid logic
    • Model checking
    • Satisfiability


    Dive into the research topics of 'The complexity of hybrid logics over equivalence relations'. Together they form a unique fingerprint.

    Cite this