Bisimulations between Verbrugge models and Veltman models

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 a given Verbrugge model can be transformed into a bisimilar Veltman model.