A Companion of "Relating Strong Behavioral Equivalences for Processes with Nondeterminism and Probabilities"

TL;DR

This paper extends the spectrum of behavioral equivalences for nondeterministic and probabilistic processes, comparing variants and examining the impact of randomized schedulers on these equivalences.

Contribution

It enlarges the existing spectrum by adding new equivalences and studies the effects of randomized schedulers on these relationships.

Findings

Expanded the spectrum with new trace and decorated-trace equivalences.

Analyzed how randomized schedulers alter the spectrum.

Provided formal relationships among various behavioral equivalences.

Abstract

In the paper "Relating Strong Behavioral Equivalences for Processes with Nondeterminism and Probabilities" to appear in TCS, we present a comparison of behavioral equivalences for nondeterministic and probabilistic processes. In particular, we consider strong trace, failure, testing, and bisimulation equivalences. For each of these groups of equivalences, 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 deterministic schedulers. The established relationships are summarized in a so-called spectrum. However, the equivalences we consider in that paper are only a small subset of those considered in the original spectrum of equivalences for nondeterministic systems introduced by Rob van Glabbeek. In this companion paper we we enlarge the spectrum by considering variants of trace equivalences (completed-trace equivalences), additional decorated-trace equivalences (failure-trace, readiness, and ready-trace equivalences), and variants of bisimulation equivalences (kernels of simulation, completed-simulation, failure-simulation, and ready-simulation preorders). Moreover, we study how the spectrum changes when randomized schedulers are used instead of deterministic ones.