On the complexity of hybrid logics with binders
Balder ten Cate, Massimo Franceschet

Abstract:
Hybrid logic refers to a group of logics lying between modal and
first-order logic in which one can refer to individual states of the
Kripke structure. In particular, the hybrid logic HL(@,!) is an
appealing extension of modal logic that allows one to refer to a state
by means of nominals and to dynamically create names for states.
Unfortunately, as for the richer first-order logic, satisfiability for
HL(@,!) is undecidable and model checking for HL(@,!) is
PSPACE-complete. We carefully analyze these negative results and
establish restrictions (both syntactic and semantic) that make the
logic decidable again and that lower the complexity of the model
checking problem.