Towards Trace Metrics via Functor Lifting
Towards Trace Metrics via Functor Lifting
复制标题
通过函子提升实现跟踪指标
DOI：
10.4230/lipics.calco.2015.35
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
B. König
中科院分区：
文献类型：
--
作者：
Paolo Baldan;F. Bonchi;Henning Kerstan;B. König
我们研究了在共代数框架中推导度量迹语义的可能性。首先，我们通过确定自然变换、单子和分配律可以被提升的条件，推广了一种从集合的范畴集系统提升函子到伪度量空间的范畴PMet的技术。通过利用最近在抽象确定方面的一些工作，这些结果可以从Set中的余代数开始推导跟踪度量。更确切地说，对于集合中的一个协代数，我们确定了它，从而得到了单数列的Eilenberg-Moore范畴中的一个协代数。当单子可以提升到PMet时，我们可以为最终的协代数配备一个行为距离。原始协代数的两种状态之间的迹距是它们在确定的协代数中的图像之间的距离，以单轴为单位。我们展示了我们的框架如何应用于不确定性自动机和概率自动机。
We investigate the possibility of deriving metric trace semantics in a coalgebraic framework. First, we generalize a technique for systematically lifting functors from the category Set of sets to the category PMet of pseudometric spaces, by identifying conditions under which also natural transformations, monads and distributive laws can be lifted. By exploiting some recent work on an abstract determinization, these results enable the derivation of trace metrics starting from coalgebras in Set. More precisely, for a coalgebra in Set we determinize it, thus obtaining a coalgebra in the Eilenberg-Moore category of a monad. When the monad can be lifted to PMet, we can equip the final coalgebra with a behavioral distance. The trace distance between two states of the original coalgebra is the distance between their images in the determinized coalgebra through the unit of the monad. We show how our framework applies to nondeterministic automata and probabilistic automata.