The complexity of hybrid logics over equivalence relations

Martin Mundhenk, Thomas Schneider

    Research output: Contribution to journalArticlepeer-review

    37 Downloads (Pure)

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

    Keywords

    • Downarrow operator
    • Hybrid logic
    • Model checking
    • Satisfiability

    Fingerprint

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

    Cite this