Probabilistic Trace and Testing Semantics: The Importance of Being Coherent

It is well known that trace and testing semantics over nondeterministic and probabilistic processes are influenced by the class of schedulers used to resolve nondeterministic choices. In particular, it is the capability of suitably limiting the power of the considered schedulers that guarantees the validity of a number of desirable properties of those semantics. Among such properties we mention the fact of being coarser than bisimulation semantics, the fact of being a congruence with respect to typical process operators, and the fact of coinciding with the corresponding semantics when restricting to fully nondeterministic or fully probabilistic processes. In this monograph, we recall various approaches against almighty schedulers appearing in the literature, we survey structure-preserving and structure-modifying resolutions of nondeterminism by providing a uniform definition for them, and we present an overview of behavioral equivalences for nondeterministic and probabilistic processes along with some anomalies affecting trace and testing semantics. We then introduce the notion of coherent resolution, which prevents a scheduler from selecting different continuations in equivalent states of a process, so that the states to which they correspond in any resolution of the process have equivalent continuations too. We show that coherency avoids anomalies related to the discriminating power, the compositionality, and the backward compatibility of probabilistic trace post-equivalence and pre-equivalence, which are variants of trace semantics. Moreover, we exhibit an alternative characterization of the former based on coherent trace distributions and an alternative characterization of the latter relying on coherent weighted trace sets. We finally extend the notion of coherent resolution by adding suitable transition decorations and prove that this ensures the insensitivity of probabilistic testing equivalence to the moment of occurrence of nondeterministic or probabilistic choices among identical actions, thus enhancing the backward compatibility of testing semantics.