# Qais

Quantitative analysis of interacting systems: foundations and algorithms

## 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

r6 - 06 Jan 2012 - 13:08:11 - AlexandraSilva