## T2 - Coalgebraic Metric Bisimulation

Bisimulations are an extremely useful tool
for reasoning about the equivalence of systems: in order to prove that two
systems are behaviourally equivalent, it is enough to provide a bisimulation
relating them. The theory of coalgebras provides a general definition of
bisimulation [Rut00].

The growing interest in quantitative properties has motivated the definition of
quantitative models and related notions of behavioural
equivalences (e.g., [LS,JY,SL]). For many quantitative properties, equivalences are
somehow inadequate since they only allow ``boolean reasoning'': either two systems are
equivalent or they are not. As an example, consider the systems S and Sε, where the
latter is like S but with ε-perturbations on quantities. These systems do not behave
exactly the same but, for small ε, they behave almost the same, meaning that the
behavior of Sε converges to the behaviour of S when ε tends to 0.

Motivated by these considerations, many authors have recently proposed several
behavioural metrics or closely related notions (e.g. [DGJP,vBW,PHW]). Differently
from the ordinary equivalences, behavioural metrics express the distance between the
behaviours of systems: if the distance is 0, then the systems are behaviourally
equivalent. Amongst the several proposals, the approach of [DJGP,PHW] is relevant for our proposal. In these papers, they define a pseudometric like Milner-Park's
bisimilarity: it is the greatest fixpoint of a monotone function Phi over the
(partially ordered) set of metrics. The function Phi relies on the so called Kantorovich
metric (also known as Hutchinson, Varstein, transport and earthmover's
metric).

Following [Rut98,Wor], we hope to get an abstract notion of metric bisimulation that corresponds to the post-fixed point of the function Phi (described above). These are, in our opinion,
extremely innovative and powerful tools for over-approximating the distance of
two systems. More formally, if R is a metric bisimulation and dF is the behavioural
metric, then R(S1,S2)=ε implies that dF(S1,S2)<=ε.

Recently, in [Mon] the linear spectrum of equivalences was characterized by relaxing the notion of finality to a weaker notion of quasi-finality. This notion, when extended to the metric setting, will provide coarser equivalences than that of bisimilarity.

Main contributions:

- a notion of coalgebraic metric bisimulation for a large class of systems (in particular, for the ones considered in T1)
- a linear spectrum for metric equivalences

**Deliverables**: Similarly to T1, this task is of foundational character, and, therefore, the main deliverable will be 3 research papers, two of which in a mainstream TCS conference (such as CONCUR, STACS or CALCO) and the other in a journal (such as TCS, MSCS, Information & Computation) plus a PhD and a master thesis.

**Research team**: LM,AMS,LSB,JNO,EF,APM,NO,BI2