Towards Trace Metrics via Functor Lifting
Reference
Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König. Towards trace metrics via functor lifting. In Lawrence S. Moss and Paweł Sobociński, editors, 6th Conference on Algebra and Coalgebra in Computer Science (CALCO'15), volume 35 of Leibniz International Proceedings in Informatics (LIPIcs), pages 35–49. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, oct 2015.
Abstract
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, showing under which conditions 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 on 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.
Keywords:
trace metric, functor lifting, pseudometric, coalgebra
Suggested BibTeX entry:
@inproceedings{BBKK15,
author = {Paolo Baldan and Filippo Bonchi and Henning Kerstan and Barbara K{\"o}nig},
booktitle = {6th Conference on Algebra and Coalgebra in Computer Science (CALCO'15)},
editor = {Lawrence S. Moss and Pawe{\l} Soboci{\'n}ski},
month = {oct},
pages = {35--49},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
title = {Towards Trace Metrics via Functor Lifting},
volume = {35},
year = {2015}
}
