Decidability of multi-modal logic $LTK$ of linear time and knowledge

The paper investigates modal (temporal-model) logics based at a semantic approach with models combining knowledge and time. We introduce multi-modal logics $LTK_r$ and $LTK_{ir}$ containing modalities for knowledge and time as the sets of all $LTK_r$-valid, and $LTK_{ir}$-valid formulae for a class of special $LTK_r$- frames, $LTK_{ir}$-frames, respectively. The main results of this paper are theorems stating that $LTK_r$ and $LTK_{ir}$ are decidable; we also give an explicit solving algorithm.