Bisimulation Invariance and Finite Models

We study bisimulation invariance over finite structures. This investigation leads to a new, quite elementary proof of the van Benthem-Rosen characterisation of basic modal logic as the bisimulation invariant fragment of first-order logic. The ramification of this characterisation for the finer notion of global twoway bisimulation equivalence is based on bisimulation respecting constructions of models that recover in finite models some of the desirable properties of the usually in finite bisimilar unravellings