Fully abstract characterizations of testing preorders for probabilistic processes

We present alternative characterizations of the testing preorders for probabilistic processes proposed in [CSZ92]. For a given probabilistic process, the characterization takes the form of a mapping from probabilistic traces to the interval [0, 1], where a probabilistic trace is an alternating sequence of actions and probability distributions over actions. Our results, like those of [CSZ92], pertain to divergence-free probabilistic processes, and are presented in two stages: probabilistic tests without internal τ-transitions are considered first, followed by probabilistic tests with τ-transitions. In each case, we show that our alternative characterization is fully abstract with respect to the corresponding testing pre-order, thereby resolving an open problem in [CSZ92]. In the second case, we use the alternative characterization to show that the testing preorder is actually an equivalence relation. Finally, we give proof techniques, derived from the alternative characterizations, for establishing preorder relationships between probabilistic processes. The utility of these techniques is demonstrated by means of some simple examples.