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.
