Non-expansive ϵ-bisimulations for probabilistic processes

ϵ-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 ϵ-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 si and ti is ϵi, then the behavioral distance between f(s1,…,sn) and f(t1,…,tn) is no more that ϵ1+⋯+ϵn. As expected, the stronger the ϵ-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 ϵ-bisimulation and actionϵ-bisimulation, arguing that global ϵ-bisimulation is not needed in such a context.