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$扩充的带逆命题动态逻辑具有有限模型性质。