Compositional testing preorders for probabilistic processes

Publisher Website
Google Scholar
Abstract
Transition 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 non-probabilistic systems to a probabilistic setting. In this paper, 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 non-probabilistic systems, these preorders collapse to the standard simulation and refusal- simulation.

This publication has 24 references indexed in Scilit: