Fuzzy logic extends the classical truth values "true" and "false" with additional truth degrees in between. More specifically, fuzzy modal logics in this sense are given by a choice of fuzzy modalities and a fuzzy propositional base. It has been noted that fuzzy modal logics over the Zadeh base, which interprets disjunction as maximum, are often computationally tractable but on the other hand add little in the way of expressivity to their classical counterparts. Contrastingly, fuzzy modal logics over the more expressive Lukasiewicz base have attractive logical properties but are often computationally less tractable or even undecidable. In the basic case of the modal logic of fuzzy relations, sometimes termed fuzzy ALC, it has recently been shown that an intermediate non-expansive propositional base, known from characteristic logics for behavioural distances of quantitative systems, strikes a balance between these poles: It provides increased expressiveness over the Zadeh base while avoiding the computational problems of the Lukasiewicz base, in fact allowing for reasoning in PSpace. Modal logics, in particular fuzzy modal logics, generally vary widely in terms of syntax and semantics, involving, for instance, probabilistic, preferential, or weighted structures. Coalgebraic modal logic provides a unifying framework for wide ranges of semantically different modal logics, both two-valued and fuzzy. In the present work, we focus on non-expansive coalgebraic fuzzy modal logics, providing a criterion for decidability in PSpace. Using this criterion, we recover the mentioned complexity result for non-expansive fuzzy ALC and moreover obtain new PSpace upper bounds for various quantitative modal logics over probabilistic and metric transition systems. Notably, we show that the logic of generally, which has recently been shown to characterize e-distance on Markov chains, is decidable in PSpace.
翻译:模糊逻辑将经典真值“真”与“假”扩展为包含介于两者之间的真度。更具体而言,此意义上的模糊模态逻辑由模糊模态词的选择与模糊命题基共同定义。已有研究指出,基于Zadeh基(将析取解释为最大值)的模糊模态逻辑通常计算上易于处理,但在表达力方面较其经典对应逻辑提升甚微。相比之下,基于更具表达力的Lukasiewicz基的模糊模态逻辑虽具有吸引人的逻辑性质,但计算上往往较难处理甚至不可判定。在模糊关系模态逻辑(有时称为模糊ALC)的基本情形中,近期研究表明,一种源自定量系统行为距离特征逻辑的中间型非扩张命题基,在上述两极之间取得了平衡:它在提供比Zadeh基更强表达力的同时,避免了Lukasiewicz基的计算难题,实际上允许在PSpace复杂度内进行推理。模态逻辑(尤其是模糊模态逻辑)通常在语法和语义上差异巨大,涉及例如概率、偏好或加权结构。共代数模态逻辑为广泛语义各异的模态逻辑(包括二值与模糊逻辑)提供了统一框架。在本工作中,我们聚焦于非扩张共代数模糊模态逻辑,提出了PSpace可判定性的判定准则。利用该准则,我们不仅重现了非扩张模糊ALC的已知复杂度结果,还进一步为概率及度量转移系统上的多种定量模态逻辑获得了新的PSpace上界。值得注意的是,我们证明了最近被证明可刻画马尔可夫链上e-距离的“一般性逻辑”在PSpace内可判定。