一句话：提出松弛耦合构造，为余代数系统定义行为距离与前序，扩展其可表达范围。
行为一致性（如行为等价、行为距离、行为前序）可在通用余代数框架下统一处理。已有的行为距离构造推广 Wasserstein 度量，将概率分布的耦合替换为依赖系统类型函子的更一般耦合；但当两个函子元素之间不存在耦合时，即使语义上不应如此，也会得到无穷距离。本文提出一种更宽松的耦合概念：允许被耦合元素以松弛方式匹配，而非必须逐点精确匹配，并据此定义行为距离和行为前序。该推广显著扩大了可用耦合表达的行为一致性的范围，可覆盖模态迁移系统的 refinement 以及度量标记 Markov 链上的行为距离等情形。
Behavioural conformances – e.g. behavioural equivalences, distances, preorders – on a wide range of system types (non-deterministic, probabilistic, weighted etc.) can be dealt with uniformly in the paradigm of universal coalgebra. One of the most commonly used constructions for defining behavioural distances on coalgebras arises as a generalization of the well-known Wasserstein metric. In this construction, couplings of probability distributions are replaced with couplings of more general objects, depending on the functor describing the system type. In many cases, however, the set of couplings of two functor elements is empty, which causes such elements to have infinite distance even in situations where this is not desirable. We propose an approach to defining behavioural distances and preorders based on a more liberal notion of coupling where the coupled elements are matched laxly rather than on-the-nose. We thereby substantially broaden the range of behavioural conformances expressible in terms of couplings, covering, e.g., refinement of modal transition systems and behavioural distance on metric labelled Markov chains.
DOI 原文 ·
@inproceedings{paperbot8649,
title = {Behavioural Conformances based on Lax Couplings},
author = {Paul Wild and Lutz Schröder},
booktitle = {LICS},
year = {2025},
doi = {10.1109/lics65433.2025.00065}
}