Non-expansive ε-bisimulations for probabilistic processes

epsilon-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 first consider the generative model of probabilistic processes and introduce two stronger equivalence notions: action epsilon-bisimulation and global epsilon-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 epsilon(i) then the behavioral distance between f (s(1), ..., s(n)) and f(t(1), ... t(n)) is no more that epsilon(1) + ... + epsilon(n). As expected, the stronger the epsilon-bisimulation considered, the weaker the constraints of the transition rule format. Then, we switch to the reactive model of probabilistic processes and we propose a rule format for epsilon-bisimulation and action epsilon-bisimulation, arguing that global epsilon-bisimulation is not needed in such a context. (C) 2010 Elsevier B.V. All rights reserved.