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.