Coalgebraic Reasoning for Quantitative System Analysis

模态逻辑作为一种形式主义，用于描述由各种被认为是状态、世界或个体的节点组成的系统，以及这些节点之间在广义上的相互关系。它广泛应用于从并发到知识表示的各种上下文中。定量模态逻辑偏离了标准的二值设置，因为它们在一个允许在完全真和完全假之间的真度的域中取真值。实单位区间是这种真值域的一个典型例子。例如，在模糊逻辑中，这个领域的真值可以被理解为表达模糊的资格，例如人很高。然而，真值的实值性也出现在其他情况下，例如在概率系统中，或者在状态或转移带有从给定度量空间中获取的标签的系统中。更一般地说，允许测量真值之间偏差的真域被有效地抽象为所谓的量子。CoRSA的目标是在这个意义上为定量模态逻辑提供自动推理支持，旨在实现推理算法在系统类型（概率、基于游戏、度量等）和模态语义上的通用性。它的范围从“有一些继承者/所有继承者”类型的模糊关系模式，超过基于期望的“可能”类型的概率模式，到基于博弈的“给定代理联盟可以强制执行某些定量属性”类型的模式。为此，我们将在通用协代数的通用框架下工作，更具体地说，是协代数逻辑，它为系统类型和模态提供了范畴抽象。从模糊描述逻辑的推理工作中，我们知道定量模态逻辑的计算性质很大程度上依赖于包含哪些命题连接词，以至于某些命题基的推理问题变得不可判定。最近关于定量模态逻辑和行为距离概念之间的联系的研究表明，可以通过关注非扩张性命题操作来找到表达性和计算可追溯性之间的平衡点，我们将在项目中澄清这一点。因此，我们期望为定量模态逻辑提供一个通用框架，该框架与行为距离的语义概念保持接近，并允许在合理的复杂性下自动演绎。

Modal logic serves as a formalism for the description of systems composed of nodes variously thought of as states, worlds, or individuals, and the interrelation between such nodes in a broad sense. It is widely applied in diverse contexts ranging from concurrency to knowledge representation. Quantitative modal logics deviate from the standard two-valued setup in that they take truth values in a domain that allows for degrees of truth in between complete truth and complete falsity. A typical example of such a domain of truth values is the real unit interval. Truth values in this domain may be read, for instance, as expressing vague qualifications, such as person being tall, in the vein of fuzzy logic. However, real-valuedness of truth arises also in other contexts, e.g. in probabilistic systems or in systems where states or transitions carry labels taken from a given metric space. More generally, truth domains that allow for measuring the deviation between truth values are usefully abstracted as so-called quantales. The object of CoRSA is to provide automated reasoning support for quantitative modal logics in this sense, aiming for genericity of reasoning algorithms over the system type (probabilistic, game-based, metric etc.) and over the semantics of the modalities, which in turn range from fuzzy relational modalities of the type `there is some successor / for all successors' over expectation-based probabilistic modalities of the type 'probably' to game-based modalities of the type a given coalition of agents can enforce some quantitative property'. To this end, we will work in the generic framework of universal coalgebra and, more specifically, coalgebraic logic, which provide categorical abstractions for the system type and the modalities. From work on reasoning in fuzzy description logics, it is known that the computational properties of quantitative modal logics depend rather strongly on which propositional connectives are included, up to the point that some reasoning problems become undecidable for certain propositional bases. Recent work on the connection between quantitative modal logics and notions of behavioral distance suggests that a point of balance between expressiveness and computational tractability may be found by focusing on non-expansive propositional operations, a point that we will clarify in the project. We thus expect to provide a generic framework for quantitative modal logics that stays close to semantic notions of behavioral distance and allows automated deduction in reasonable complexity.