Denotational Semantics for Probabilistic Refusal Testing

AbstractIn this paper, refusal testing ideas are applied to define a testing semantics for a probabilistic process algebra. A testing equivalence is defined by combining the greater discriminatory power of refusal testing and a simple treatment of the probabilistic component of processes. This testing equivalence is characterized by two fully abstract denotational semantics. The first of them is based on probabilistic refusal traces. These traces condense the set of tests that a process passes with probability greater than zero. The second one is based on a probabilistic extension of classical acceptance trees, where semantic processes can be viewed as (syntactic) normal forms.We would like to thank the anonymous referees of this paper for their valuable comments, specially one who pointed out a mistake in a previous version