ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Sun 7 Apr 2019 15:00 - 15:30 at S7 - Session III

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.

Sun 7 Apr

14:00 - 15:30: QAPL - Session III at S7
qapl-2019-papers14:00 - 15:00
qapl-2019-papers15:00 - 15:30
Marco BernardoUniversity of Urbino