COALGEBRAIC BEHAVIORAL METRICS
COALGEBRAIC BEHAVIORAL METRICS
复制标题
DOI：
10.23638/lmcs-14(3:20)2018
复制
发表时间：
2018-01-01
影响因子：
0.6
通讯作者：
Koenig, Barbara
中科院分区：
文献类型：
--
作者：
Baldan, Paolo;Bonchi, Filippo;Koenig, Barbara
我们研究了不同的行为指标，如所产生的分支ing和线性时间语义，在一个coalgebraic设置。给定一个余代数α：X -> HX（对于函子H：Set -> Set），定义了一个在X上构造度量状态行为距离的伪度量的框架，其中关键的一步是将Set上的函子H提升为伪度量空间范畴PMet上的函子（H）.我们提出了两种不同的方法，可以被看作是推广的Kantorovich和Wasserstein伪度量的概率措施。我们证明了这两种方法所提供的伪度量在几个自然例子上是一致的，但一般来说它们是不同的。如果H有最终余代数，则在bar上的每个提升（H）以规范的方式产生一个行为距离，该距离通常是分支时间，即，它推广了双相似性。为了模拟线性时间度量（广义迹等价），我们证明了提升分配律和单子的充分条件。这些结果使我们能够采用广义幂集结构。
We study different behavioral metrics, such as those arising from both branch ing and linear-time semantics, in a coalgebraic setting. Given a coalgebra alpha: X -> HX for a functor H: Set -> 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 Set to a functor (H) over bar on the category 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 (H) over bar yields in a canonical way a behavioral distance which is usually branching-time, i.e., it generalizes bisimilarity. In order to model lineartime metrics (generalizing trace equivalences), we show sufficient conditions for lifting distributive laws and monads. These results enable us to employ the generalized powerset construction.