Transformation of any Verbrugge model to a bisimilar Veltman model

Veltman semantics is the basic Kripke-like semantics for interpretability logic. Verbrugge semantics is a generalization of Veltman semantics. An appropriate notion of bisimulation between a Verbrugge model and a Veltman model is developed in this paper. We show that each Verbrugge model can be transformed to a bisimilar Veltman model.