10.23638/LMCS-14(3:20)2018
https://lmcs.episciences.org/4715
Baldan, Paolo
Paolo
Baldan
Bonchi, Filippo
Filippo
Bonchi
Kerstan, Henning
Henning
Kerstan
König, Barbara
Barbara
König
Coalgebraic Behavioral Metrics
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.
episciences.org
Computer Science - Logic in Computer Science
2018-09-14
2018-09-14
2018-09-14
eng
journal article
arXiv:1712.07511
10.48550/arXiv.1712.07511
1860-5974
https://lmcs.episciences.org/4715/pdf
VoR
application/pdf
Logical Methods in Computer Science
Volume 14, Issue 3
Researchers
Students