A complete classification of the complexity of the local and global satisfiability problems for graded modal language over traditional classes of frames have already been established. By "traditional" classes of frames, we mean those characterized by any positive combination of reflexivity, seriality, symmetry, transitivity, and the Euclidean property. In this paper, we fill the gaps remaining in an analogous classification of the graded modal language with graded converse modalities. In particular, we show its NExpTime-completeness over the class of Euclidean frames, demonstrating this way that over this class the considered language is harder than the language without graded modalities or without converse modalities. We also consider its variation disallowing graded converse modalities, but still admitting basic converse modalities. Our most important result for this variation is confirming an earlier conjecture that it is decidable over transitive frames. This contrasts with the undecidability of the language with graded converse modalities.
翻译:已经确定了对传统框架类别中按等级划分的模式语言的当地和全球可比较性问题的复杂性的完整分类。 “ 传统”框架类别是指反应性、序列性、对称性、过渡性以及欧几里德属性的任何积极组合。 在本文中,我们用等级对等模式语言的类似分类方式填补了与等级对立模式语言的类似分类方式的剩余空白。特别是,我们展示了在欧几里德框架类别中,所考虑的语言比不按等级划分的方式或没有相反方式的语言更难。我们还考虑其变异性,不允许分级对立方式,但仍然接受基本的对立方式。我们这一变异的最重要结果就是证实早先的推论,即它对于等级对等框架来说是可分化的。这与语言与分级对立方式的不衰变性形成对比。