一句话：在余代数框架下统一构造行为伪度量，推广 Kantorovich/Wasserstein 度量并涵盖分支时间与线性时间语义。
论文研究如何在余代数统一框架中定义状态之间的行为距离，包括分支时间（如互模拟）和线性时间（如迹等价）语义对应的度量。给定集合函子 H 上的余代数 α:X→HX，作者提出将 H 提升到伪度量空间范畴 PMet 的框架，并给出两类提升方法，可视为概率测度的 Kantorovich 与 Wasserstein 伪度量的推广。结果表明两者在若干自然例子上一致，但一般情况下不同；若 H 有终结余代数，每种提升都典范地诱导出通常为分支时间的行为距离。为处理线性时间度量，作者给出提升分配律与单子的充分条件，并借助广义幂集构造实现。
We study different behavioral metrics, such as those arising from both branching and linear-time semantics, in a coalgebraic setting. Given a coalgebra $\alpha\colon X \to HX$ for a functor $H \colon \mathrm{Set}\to \mathrm{Set}$, we define a framework for deriving pseudometrics on $X$ which measure the behavioral distance of states. A crucial step is the lifting of the functor $H$ on $\mathrm{Set}$ to a functor $\overline{H}$ on the category $\mathrm{PMet}$ of pseudometric spaces. We present two different approaches which can be viewed as generalizations of the Kantorovich and Wasserstein pseudometrics for probability measures. We show that the pseudometrics provided by the two approaches coincide on several natural examples, but in general they differ. If $H$ has a final coalgebra, every lifting $\overline{H}$ yields in a canonical way a behavioral distance which is usually branching-time, i.e., it generalizes bisimilarity. In order to model linear-time metrics (generalizing trace equivalences), we show sufficient conditions for lifting distributive laws and monads. These results enable us to employ the generalized powerset construction.
@article{paperbot377,
title = {Coalgebraic Behavioral Metrics},
author = {Paolo Baldan and Filippo Bonchi and Henning Kerstan and Barbara König},
journal = {Logical Methods in Computer Science},
volume = {Volume 14, Issue 3},
year = {2018},
doi = {10.23638/lmcs-14(3:20)2018}
}