Kantorovich函子与行为距离的特征逻辑
Kantorovich Functors and Characteristic Logics for Behavioural Distances
AI总结：
本文在共代数框架下研究量化系统的行为距离，证明所有保持等距映射的函子提升及quantale值度量空间函子均为Kantorovich型，可通过量化模态逻辑刻画其诱导的行为距离，推广了松弛扩展相关结论。
摘要：
行为距离用于衡量量化系统（如概率系统或加权系统）中状态之间的偏差。目前人们对行为距离的通用方法越来越感兴趣。具体而言，共代数方法能够涵盖系统类型的差异（非确定性、概率性、基于博弈的等），而quantale（格化半群）的概念则对距离的实际取值进行了抽象，因此可以覆盖例如二值等价、（伪）度量以及概率（伪）度量等多种情形。\n共代数行为距离要么基于将SET（集合范畴）函子提升到度量空间范畴，要么基于将SET函子松弛扩展到量化关系范畴。每个松弛扩展都能诱导一个函子提升，但并非每个提升都源自松弛扩展。近期研究表明，每个松弛扩展都是Kantorovich型的，即由适当选择的单调谓词提升诱导，这通过量化共代数Hennessy-Milner定理意味着：由松弛扩展诱导的行为距离可以用量化模态逻辑来刻画。\n本文在更一般的由函子提升诱导的行为距离框架下，本质上证明了相同的结论。具体来说，我们证明了每个保持等距映射的函子提升，乃至每个（quantale值）度量空间上的函子，都是Kantorovich型的，因此（在分支度受适当限制的系统上）其诱导的行为距离可以用量化模态逻辑来刻画。
英文摘要：
Behavioural distances measure the deviation between states in quantitative systems, such as probabilistic or weighted systems. There is growing interest in generic approaches to behavioural distances. In particular, coalgebraic methods capture variations in the system type (nondeterministic, probabilistic, game-based etc.), and the notion of quantale abstracts over the actual values distances take, thus covering, e.g., two-valued equivalences, (pseudo-)metrics, and probabilistic (pseudo-)metrics. Coalgebraic behavioural distances have been based either on liftings of SET-functors to categories of metric spaces, or on lax extensions of SET-functors to categories of quantitative relations. Every lax extension induces a functor lifting but not every lifting comes from a lax extension. It was shown recently that every lax extension is Kantorovich, i.e. induced by a suitable choice of monotone predicate liftings, implying via a quantitative coalgebraic Hennessy-Milner theorem that behavioural distances induced by lax extensions can be characterized by quantitative modal logics. Here, we essentially show the same in the more general setting of behavioural distances induced by functor liftings. In particular, we show that every functor lifting, and indeed every functor on (quantale-valued) metric spaces, that preserves isometries is Kantorovich, so that the induced behavioural distance (on systems of suitably restricted branching degree) can be characterized by a quantitative modal logic.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
