Testing and Refinement for Nondeterministic and Probabilistic Processes

. Transition systems are a basic semantic model for formal description, specification, and analysis of concurrent and distributed systems. In order to describe and analyze aspects of reliability, such as the likelihood of trace and failure, this model has been extended in various ways to handle probabilistic behavior. To use these models for specification and stepwise development of systems, it is important to develop appropriate refinement preorders. In the paper, we develop refinement preorders based on a framework of testing for a model that represents both nondeterministic and probabilistic choices as independent concepts [YL92]. Our main contribution is a notion of reward testing, and a denotational characterization of a testing preorder, which corresponds to a natural probabilistic extension of the trace model [Hoa85]. 1 Introduction Transition systems are well-established as a basic semantic model for the formal description, specification, and analysis of concurrent and distrib..