Coherent Resolutions of Nondeterminism

We study the impact that different ways of resolving nondeterminism within probabilistic automata have on the properties of probabilistic behavioral equivalences. Firstly, we provide a uniform definition of structure-preserving and structure-modifying resolutions of nondeterminism, respectively generated by different families of schedulers. Secondly, we exhibit a number of anomalies arising from the excessive power of the various families of schedulers, which affect the discriminating power, the compositionality, and the backward compatibility of probabilistic trace equivalence. Thirdly, we propose to remove those anomalies by enforcing coherency within resolutions of nondeterminism. This ensures that a scheduler cannot select different continuations in equivalent states of an automaton, so that also the states to which they correspond in any resolution of the automaton have equivalent continuations.