Information Technology Reference
In-Depth Information
4.8
Bibliographic Notes
Probabilistic extensions of testing equivalences [ 1 ] have been widely studied. There
are two different proposals on how to include probabilistic choice: (i) a test should be
nonprobabilistic, i.e. there is no occurrence of probabilistic choice in a test [ 10 - 14 ];
or (ii) a test can be probabilistic, i.e. probabilistic choice may occur in tests as well
as processes [ 3 , 4 , 15 - 19 ]. This topic adopts the second approach.
Some work [ 10 , 11 , 15 , 16 ] does not consider nondeterminism but deals exclu-
sively with fully probabilistic processes. In this setting, a process passes a test with a
unique probability instead of a set of probabilities, and testing preorders in the style
of [ 1 ] have been characterised in terms of probabilistic traces [ 15 ] and probabilistic
acceptance trees [ 16 ].
Generalisations of the testing theory of [ 1 ] to probabilistic systems first appear
in [ 11 ] and [ 20 ], for generative processes without nondeterministic choice. The
application of testing to the probabilistic processes we consider here stems from [ 3 ].
The idea of vector-based testing originally comes from [ 4 ].
In [ 21 ], reactive processes are tested against three classes of tests: reactive prob-
abilistic tests, fully nondeterministic tests, and nondeterministic and probabilistic
tests. Thus three testing equivalences are obtained. It is shown that the one based on
the third class of tests is strictly finer than the first two, which are incomparable with
each other.
In [ 12 ], a testing theory is proposed that associates a reward , a nonnegative real
number, to every success state in a test process; in calculating the set of results of ap-
plying a test to a process, the probabilities of reaching a success state are multiplied
by the reward associated to that state. [ 12 ] allows nonprobabilistic tests only, but
applies these to arbitrary nondeterministic probabilistic processes, and provides a
trace-like denotational characterisation of the resulting may-testing preorder. Deno-
tational characterisations of the variant of our testing preorders in which only ˄ -free
processes are allowed as test processes appear in [ 17 , 22 ]. These characterisations
are improved in [ 18 ].
In [ 19 ], a testing theory for nondeterministic probabilistic processes is developed
in which, as in [ 23 ], all probabilistic choices are resolved first. A consequence of
this is that the idempotence of internal choice must be sacrificed. The work [ 19 ]
extends the results of [ 16 ] with nondeterminism, but suffers from the same problems
as [ 23 ]. Similarly, in [ 24 ], probabilistic choices are resolved first and the resulting
resolutions are compared under the traditional testing semantics of [ 1 ]. Some papers
distill preorders for probabilistic processes by means of testing scenarios in which
the premise that a test is itself a process is given up. These include [ 10 , 13 ] and [ 25 ].
In our testing framework given in Sect. 4.1 , applying a test to a process yields a
composite process from which success probabilities are extracted cumulatively on
all resolutions. In [ 26 ], a different testing framework is presented where success
probabilities are considered in a trace-by-trace fashion. Different variants of testing
equivalences are compared and placed in spectrum of trace and testing equivalences.
Search WWH ::




Custom Search