Relating strong behavioral equivalences for processes with nondeterminism and probabilities

We present a comparison of behavioral equivalences for nondeterministic and probabilistic processes whose activities are all observable. In particular, we consider trace-based, testing, and bisimulation-based equivalences. For each of them, we examine the discriminating power of three variants stemming from three approaches that differ for the way probabilities of events are compared when nondeterministic choices are resolved via schedulers. The first approach compares two resolutions with respect to the probability distributions of all considered events. The second approach requires that the probabilities of the set of events of a resolution be individually matched by the probabilities of the same events in possibly different resolutions. The third approach only compares the extremal probabilities of each event stemming from the different resolutions. The three approaches have very reasonable motivations and, when applied to fully nondeterministic processes or fully probabilistic processes, give rise to the classical well studied relations. We shall see that, for processes with nondeterminism and probability, they instead give rise to a much wider variety of behavioral relations, whose discriminating power is thoroughly investigated here in the case of deterministic schedulers