We study different behavioral metrics, such as those arising from both branching and linear-time semantics, in a coalgebraic setting. Given a coalgebra α : 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' 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' 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.

Coalgebraic Behavioral Metrics

Paolo Baldan;
2018

Abstract

We study different behavioral metrics, such as those arising from both branching and linear-time semantics, in a coalgebraic setting. Given a coalgebra α : 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' 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' 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.
2018
File in questo prodotto:
File Dimensione Formato  
LMCS-Probability-2018.pdf

accesso aperto

Descrizione: Copia PDF
Tipologia: Published (publisher's version)
Licenza: Accesso gratuito
Dimensione 717.92 kB
Formato Adobe PDF
717.92 kB Adobe PDF Visualizza/Apri
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11577/3278793
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 33
  • ???jsp.display-item.citation.isi??? 19
  • OpenAlex ND
social impact