Real-Reward Testing for Probabilistic Processes
                     

   Yuxin Deng, Rob van Glabbeek, Matthew Hennessy, and Carroll Morgan

We introduce a notion of real-valued reward testing for probabilistic
processes by extending the traditional nonnegative-reward testing with
negative rewards. In this richer testing framework, the may and must
preorders turn out to be inverses.  We show that for convergent
processes with finitely many states and transitions, but not in the
presence of divergence, the real-reward must-testing preorder
coincides with the nonnegative-reward must-testing preorder. To prove
this coincidence we characterise the usual resolution-based testing in
terms of the weak transitions of processes, without having to involve
policies, adversaries, schedulers, resolutions, or similar structures
that are external to the process under investigation. This requires
establishing the continuity of our function for calculating testing
outcomes.