In Martin Otto's paper "Elementary proof of Van Benthem-Rosen Characterisation Theorem" I've found this lemma:
Lemma 2.1. Over the class of all Kripke structures of a finite fixed relational type:
(i) $\sim_{l}$ has finite index
(ii) $\mathfrak{A},a\sim_{l}\mathfrak{B},b$ iff $a\in\mathfrak{A}$ and $b\in\mathfrak{B}$ are indistinguishable in $ML_{l}$
(iii) each $\sim_{l}$ equivalence class is definable by an $ML_{l}$ formula.
$\sim_{l}$ stands for l-bisimulation, and $ML_{l}$ stands for all formulas of propositional modal logic which have modal depth at most $l$. Furthermore, Otto says that this lemma is consequence of Ehrenfeucht - Fraisse analysis of bisimulation game. Does anyone can recommend some book where I can find proof for this lemma or offer any hint? I understand what bisimulation game is, but I have trouble understanding what is l-bisimulation and its relation to ordinary bisimulation.
The entry Model Theory of Modal Logic by Valentin Goranko and Martin Otto in Handbook of Modal Logic, Blackburn, van Benthem and Wolter (eds.), Elsevier 2007 covers this territory.
A final draft of the chapter may be downloaded from Goranko's website.