Acceptance trees for probabilistic processes

In this paper we study the extension of classical testing theory to a probabilistic process algebra. We consider a generative interpretation of probabilities for a language with two choice operators (one internal and the other external), which are annotated with a probability p ε (0, 1). We define a testing semantics for our language, and we write P pass _p T to denote that the process P passes the test T with a probability p. We also give a set of essential tests which has the same strength as the full family of tests.Next we give an alternative characterization of the testing semantics, based on the idea of acceptance sets, and we prove that the new equivalence is equal to the testing equivalence. Finally, we present a fully abstract denotational semantics based on acceptance trees.