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.

翻译：我们在余代数框架下研究不同的行为度量，包括源于分支语义和线性时间语义的度量。给定函子$H \colon \mathrm{Set}\to \mathrm{Set}$及其对应的余代数$\alpha\colon X \to HX$，我们建立了一个推导$X$上伪度量的框架，用于度量状态间的行为距离。关键步骤是将集合范畴$\mathrm{Set}$上的函子$H$提升为伪度量空间范畴$\mathrm{PMet}$上的函子$\overline{H}$。我们提出了两种可视为概率测度Kantorovich与Wasserstein伪度量推广的研究路径。研究表明，两种方法导出的伪度量在若干自然实例中具有一致性，但在一般情形下存在差异。若$H$存在终余代数，则每个提升$\overline{H}$都能规范地导出一个通常属于分支时间范畴的行为距离（即对互模拟关系的推广）。为建立线性时间度量（推广迹等价关系），我们给出了提升分配律与幺半群的充分条件。这些结论使我们能够运用广义幂集构造方法。