This paper examines and classifies the computational complexity of modelchecking and satisfiability for hybrid logics over frames withequivalence relations. The considered languages contain all possiblecombinations of the downarrow binder, the existential binder, thesatisfaction operator, and the global modality, ranging from the minimalhybrid language to very expressive languages. For model checking, weseparate polynomial-time solvable from PSPACE-complete cases, and forsatisfiability, we exhibit cases complete for NP, PSpace, NExpTime, andeven N2ExpTime. Our analysis includes the versions of all these languageswithout atomic propositions, and also complete frames.
|Title of host publication||host publication|
|Number of pages||10|
|Publication status||Published - 2007|
|Event||HyLo 2007 - |
Duration: 1 Jan 1824 → …
|Period||1/01/24 → …|