We consider interpretability logic, a modal description of the interpretability predicate, and try to determine the most suitable notion of bisimulation for generalized Veltman semantics. In the first part of this paper we consider several notions of bisimulation and determine connections between them. In the second part we develop some further model theoretic properties for generalized Veltman semantics and consider difficulties that arise when studying quotient structures.

We obtain modal completeness of the interpretability logics IL $\!\!\textsf {P}_{\textsf {0}}$ and ILR w.r.t. generalised Veltman semantics. Our proofs are based on the notion of full labels [2]. We also give shorter proofs of completeness w.r.t. the generalised semantics for many classical interpretability logics. We obtain decidability and finite model property w.r.t. the generalised semantics for IL $\textsf {P}_{\textsf {0}}$ and ILR. Finally, we develop a construction that might be useful for proofs of completeness of extensions of ILW w.r.t. (...) the generalised semantics in the future, and demonstrate its usage with $\textbf {IL}\textsf {W}^\ast = \textbf {IL}\textsf {WM}_{\textsf {0}}$. (shrink)