Scope

Behavioural equivalences, such as bisimilarity and trace equivalence, play a central role in concurrency theory. Such an equivalence answers the fundamental question "Do (states of) systems behave the same?" This question is not only of theoretical interest, but also has practical implications in areas such as compiler optimization and program analysis. For systems that contain quantitative information, like time or probability, such a discrete notion (systems are either equivalent or they are not) does not make much sense. Minor changes in the quantitative data may cause equivalent systems to become behaviourally different and vice versa. Since the quantitative information is usually an approximation, in such a case a behavioural equivalence contains very little information, if any at all.

Instead of equivalences, several related notions have been proposed to capture the behavioural similarity of systems with quantitative features. For example, pseudometric spaces and uniform spaces have been exploited to capture behavioural similarity in a quantitative way. Behavioural equivalences can also be quantified by using an appropriate norm of a linear operator on a Hilbert space. A family of equivalence relations (one for each nonnegative real number) can also be exploited to generalize an equivalence to a quantitative setting.