Testing preorders for probabilistic processes

We present a testing preordez for probabillstic processes based on the natural notion of a process passing a test with a certain probability. The theory enjoys dose connections with the classical testing theory of Hennessy and DeNieola in that whenever a process passes a test with probabillty 1 (respectively some non-0 probability) in our setting, then the process must (respectively may) pass the test in the elassleal theory. In addition, we develop an alternative characterisation of the probabilistic testing preordex that is based on the “must sets” characterizatlon of De Nicola. Finally, we extend our theory of testing to substochestic processes, in which the sum of the probabilities ofa process’s outgoing transitions may be strictly less than 1, with the deficit representing the process’ capacity for undefined behavior. A simple example involving the construction of pipelines from faulty buffer cells is given to illustrate how substochastic processes, and the resulting preorder, can be used to model fault-tolerant systems and to reason about system reliability.