Probabilistic Trace and Testing Semantics: The Importance of Being Coherent
By Marco Bernardo, Università di Urbino, Italy, marco.bernardo@uniurb.it
Abstract
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 preequivalence, 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.
Probabilistic Trace and Testing Semantics: The Importance of Being Coherent
In this monograph, the author focuses on trace and testing semantics for nondeterministic and probabilistic processes represented by simple probabilistic automata. A trace is a sequence of activities labeling a sequence of transitions performed by a process, thus abstracting from branching points in the process behavior. A test is formalized as a nondeterministic and probabilistic process extended with success states or success actions, which is run in parallel with the process under test thus resulting in an interaction or testing system.
Written as a comprehensive review of the topic, the author introduces the reader to the concept of nondeterministic and probabilistic models and how nondeterminism can be resolved. The author then considers probabilistic models, three anomalies of these models and how to overcome them. The author then addresses alternative characterizations of the two probabilistic trace equivalences. Finally, the author considers the anomalies of probabilistic testing equivalence and how to avoid them.
This monograph is aimed at researchers working on the formal method aspects of programming languages.
