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 the given names and to dynamically create new names for a state.
Unfortunately, as for the richer first-order logic, satisfiability for the hybrid logic HL(@, ↓ ) is undecidable and model
checking for HL(@, ↓ ) is PSpace-complete. We carefully analyze these results and we isolate large fragments of HL(@, ↓ ) for which satisfiability is decidable
and model checking is below PSpace.