In the setting of nondeterministic and probabilistic processes, we study the impact that different ways of resolving nondeterminism may have on the discriminating power, the compositionality, and the backward compatibility of behavioral equivalences. After providing a uniform way of defining structure-preserving and structure-manipulating resolutions respectively generated from deterministic and randomized/interpolating schedulers, we reveal a number of anomalies of probabilistic trace equivalence due to the excessive power of schedulers. We remove those anomalies by introducing the notion of coherent resolution, which guarantees that if two states in the distribution reached by a transition possess the same traces, then so do the states to which they correspond in a resolution.
Program Display Configuration
Sun 7 Apr
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Viennachange