On partitioning Kripke frames of finite height

TL;DR

This paper establishes finite model property and decidability for certain modal logics based on pretransitive Kripke frames of finite height, through special partitionings called filtrations.

Contribution

It introduces a method for partitioning pretransitive frames of finite height, proving finite model property and decidability for the associated modal logics.

Findings

Finite model property proved for these modal logics.

Decidability established for the class of frames.

Partitioning techniques enable effective model construction.

Abstract

The paper proves finite model property and decidability for a family of modal logics. A binary relation $R$ is called pretransitive, if $R^*=\cup_{i\leq m} R^i$ for some $m\geq 0$, where $R^*$ is the transitive reflexive closure of $R$. By the height of $(W,R)$ we mean the height of the preorder $(W,R^*)$. Special partitionings (filtrations) are described for pretransitive frames of finite height, which implies finite model property and decidability of logics of these frames.