行为半度量的特征逻辑：基于模糊松弛扩展
Characteristic Logics for Behavioural Hemimetrics via Fuzzy Lax Extensions
AI总结：
本文证明所有模糊松弛扩展均可视为基于Moss模态的Kantorovich扩展，从而为非扩张情形提取出表征行为距离的定量模态逻辑，并推广至半度量（定量模拟）情形。
摘要：
在涉及定量数据的系统中，如概率系统、模糊系统或度量系统，行为距离比二值的行为等价或行为包含概念能提供更细粒度的状态比较。与二值情形类似，系统类型中的广泛差异产生了对适用于多种系统类型的通用方法的需求。此类方法正在泛代数（universal coalgebra）范式内涌现，其途径要么是沿着集合函子提升伪度量，要么是通过模糊松弛扩展（fuzzy lax extensions）沿着函子提升一般的实值（模糊）关系。后者的一个直接好处是，它允许通过模糊（双）模拟来界定行为距离，而这些模糊（双）模拟本身不必是半度量或伪度量；这类似于经典模拟和双模拟，它们分别不必是预序或等价关系。已知的通用伪度量提升，特别是通用的 Kantorovich 和 Wasserstein 提升，都可以扩展为模糊松弛扩展，利用的事实是两者实际上都由一组定量模态的选择给出。我们的核心结果随后表明，事实上所有模糊松弛扩展都是针对合适定量模态集（即所谓的 Moss 模态）的 Kantorovich 扩展。对于非扩张的模糊松弛扩展，这允许提取表征行为距离的定量模态逻辑，即满足 Hennessy-Milner 定理的定量版本；等价地，我们获得了 Moss 余代数逻辑的定量版本的表现力。我们的所有结果也明确适用于非对称距离（半度量），即定量模拟的概念。
英文摘要：
In systems involving quantitative data, such as probabilistic, fuzzy, or metric systems, behavioural distances provide a more fine-grained comparison of states than two-valued notions of behavioural equivalence or behaviour inclusion. Like in the two-valued case, the wide variation found in system types creates a need for generic methods that apply to many system types at once. Approaches of this kind are emerging within the paradigm of universal coalgebra, based either on lifting pseudometrics along set functors or on lifting general real-valued (fuzzy) relations along functors by means of fuzzy lax extensions. An immediate benefit of the latter is that they allow bounding behavioural distance by means of fuzzy (bi-)simulations that need not themselves be hemi- or pseudometrics; this is analogous to classical simulations and bisimulations, which need not be preorders or equivalence relations, respectively. The known generic pseudometric liftings, specifically the generic Kantorovich and Wasserstein liftings, both can be extended to yield fuzzy lax extensions, using the fact that both are effectively given by a choice of quantitative modalities. Our central result then shows that in fact all fuzzy lax extensions are Kantorovich extensions for a suitable set of quantitative modalities, the so-called Moss modalities. For nonexpansive fuzzy lax extensions, this allows for the extraction of quantitative modal logics that characterize behavioural distance, i.e. satisfy a quantitative version of the Hennessy-Milner theorem; equivalently, we obtain expressiveness of a quantitative version of Moss' coalgebraic logic. All our results explicitly hold also for asymmetric distances (hemimetrics), i.e. notions of quantitative simulation.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
