The Complexity of Hybrid Logics over Equivalence Relations

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. In the model-checking case,
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 also includes the versions without
atomic propositions of all these languages.