We describe a family of decidable propositional dynamic logics, where atomic modalities satisfy some extra conditions (for example, given by axioms of the logics K5, S5, or K45 for different atomic modalities). It follows from recent results (Kikot, Shapirovsky, Zolin, 2014; 2020) that if a modal logic $L$ admits a special type of filtration (so-called definable filtration), then its enrichments with modalities for the transitive closure and converse relations also admit definable filtration. We use these results to show that if logics $L_1, \ldots , L_n$ admit definable filtration, then the propositional dynamic logic with converse extended by the fusion $L_1*\ldots * L_n$ has the finite model property.
翻译:我们描述了一族可判定的命题动态逻辑,其中原子模态满足某些额外条件(例如,由逻辑K5、S5或K45针对不同原子模态的公理所给定)。根据近期成果(Kikot, Shapirovsky, Zolin, 2014; 2020),若一个模态逻辑$L$容许一种特殊类型的过滤(即可定义过滤),则其对于传递闭包和逆关系模态的扩充也容许可定义过滤。我们利用这些成果证明:若逻辑$L_1, \ldots , L_n$均容许可定义过滤,则经融合$L_1*\ldots * L_n$扩展的带逆关系的命题动态逻辑具有有限模型性质。