Non expansive ε-bisimulations

Abstract

ε-bisimulation equivalence has been proposed in the literature as a technique to study the concept of behavioral distance between probabilistic processes. In this paper we consider also two stronger equivalences: action ε-bisimulation and global ε-bisimulation. For each of these three equivalence notions we propose an SOS transition rule format ensuring the property of non-expansiveness. Non-expansiveness means that if the behavioral distance between s i and t i is ε i , then the behavioral distance between f(s 1,...,s n ) and f(t 1,...,t n ) is no more that ε 1∈+∈...∈+∈ε n . As expected, the stronger the ε-bisimulation considered, the (slightly) weaker the constraints of the transition rule format. © 2008 Springer-Verlag Berlin Heidelberg.