Decidability and Complexity of Some Interpretability Logics

The usual way to prove decidability of a modal logic with relational (Kripke-style) semantics is to prove it has the finite model property. Interpretability logics are usually interpreted on classes of Veltman models, or generalized Veltman models, which are both extensions of Kripke models. We will describe an approach to proving the finite model property by defining a certain filtration of generalized Veltman models. We use this approach to prove decidability of the logic ILM0 and ILW*. We also study computational complexity of logics based on Veltman models. We prove that the logic IL is in PSPACE ; and since it was already known to be PSPACE-hard, we conclude that it is PSPACE-complete. We will comment on complexity of some other interpretability logics with finite model property.