Testing preorders for probabilistic processes

We present a testing preorder for probabilistic processes based on a quanti fication of the probability with which processes pass tests. The theory enj oys close connections with the classical testing theory of De Nicola and He nnessy in that whenever a process passes a test with probability 1 (respect ively some nonzero probability) in our setting, then the process must (resp ectively may) pass the test in the classical theory. We also develop an alt ernative characterization of the probabilistic testing preorders that takes the form of a mapping from probabilistic traces to the interval [0, 1], wh ere a probabilistic trace is an alternating sequence of actions and probabi lity distributions over actions. Finally, we give proof techniques, derived from the alternative characterizations, for establishing preorder relation ships between probabilistic processes. The utility of these techniques is d emonstrated by means of some simple examples. (C) Press Academic Press.