Testing preorders for probabilistic processes can be characterized by simulations

AbstractTransition systems are well established as a semantic model for distributed systems. There are several preorders that serve as criteria for refinement of an abstract transition system to a more concrete one. To reason about probabilistic phenomena such as failures and randomization, we need to extend models and methods that have proven successful for nonprobabilistic systems to a probabilistic setting. In this paper, we develop a refinement preorder for a probabilistic extension of the transition systems model. The preorder is based on a notion of testing, where refinement corresponds to an improvement in the “worst-case” behavior of a process. The main result of the paper is that this preorder can be described by a notion of probabilistic simulation, which generalizes the standard simulation preorder for ordinary transition system. To our knowledge, this simulation preorder has not been previously described in the literature, and is strictly weaker than previously proposed simulations for probabilistic transition systems