Characterizations of two basic hybrid logics

Abstract We prove a van Benthem–Rosen-style characterization theorem for two basic hybrid logics: modal logic with nominals, and modal logic with nominals and @. In each case, we show that over all Kripke models, and over all finite Kripke models, every first-order formula that is invariant under the appropriate bisimulations is equivalent to a hybrid formula, and we give optimal bounds on its modal depth in terms of the quantifier depth of the first-order formula. We also show that the characterization for modal logic with nominals and @ extends to arbitrary bisimulation-closed classes of Kripke models and to the class of finite models within such classes, while the characterization for modal logic with nominals alone does not.