Classically, modal logic is seen as a fragment of first-order logic, determined by a standard translation 
of modal formulas into first-order formulas that captures Kripke semantics. This fragment was
characterized by van Benthem as containing precisely the bisimulation invariant formulas; it was later
shown by Rosen that this characterization remains true over finite models, although the tools used in
the original proof include model theoretic facts such as compactness and saturation that break down
over finite models. We refer to the former type of results (characterization over all models) as
van-Benthem-type results, and to results over finite models as Rosen-type results. 

The design of a correspondence language for coalgebraic modal logic is a delicate problem, since one
needs to include a sort for neighbourhoods to represent predicate liftings, avoiding at the same time
the full expressive power of monadic second order logic, whose bisimulation invariant fragment
includes non-modal formulas. We design such a language and prove a generic Rosen-type result
stating that every first-order formula which is invariant under behavioural equivalence is equivalent to
possibly infinitary but bounded-rank modal formula, and hence to a finitary modal formula in case the
modal similarity type is finite.