Compositional testing preorders for probabilistic processes

Transitions systems are well established as a semantic model for distributed systems. There are widely accepted preorders that serve as criteria for refinement of a more abstract transition system to a more concrete one. To reason about probabilistic phenomena such as failure rates, we need to extend models and methods that have proven successful for nonprobabilistic systems to a probabilistic setting. We consider a model of probabilistic transition systems, containing probabilistic choice and nondeterministic choice as independent concepts. We present a notion of testing for these systems. Our main contributions are denotational characterizations of the testing preorders. The characterizations are given in terms of chains for may testing and refusal chains for must testing, that are analogous to traces and failures in denotational models of CSP. Refinement corresponds to inclusion between chains and refusal chains modulo closure operations. The preorders are shown to be compositional. We also show that when restricted to nonprobabilistic systems, these preorders collapse to the standard simulation and refusal simulation