Real Reward Testing for Probabilistic Processes (Extended Abstract)

Select |




Print


Deng, Yuxin; van Glabbeek, Robert; Hennessy, Matthew; Morgan, Carroll

Deng, Yuxin; van Glabbeek, Robert; Hennessy, Matthew; Morgan, Carroll


2011-07-04


Conference Material


Ninth Workshop on Quantitative Aspects of Programming Languages (QAPL 2011)


Saarbrücken, Germany


61-73


We introduce a notion of real-valued reward testing for probabilistic processes by extending the traditional nonnegative reward testing with negative rewards. In this 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 involving 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.


Open Publishing Association


Probabilistic processes, nondeterminism, transition systems, testing equivalences, reward testing, failure simulation, divergence.


https://doi.org/10.4204/EPTCS.57.5


http://www.dcs.gla.ac.uk/qapl11/


Copyright on all papers is retained by the author, and full-text electronic access to all papers is freely available, without any need for registration or subscription.


nicta:3864


Deng, Yuxin; van Glabbeek, Robert; Hennessy, Matthew; Morgan, Carroll. Real Reward Testing for Probabilistic Processes (Extended Abstract). In: Mieke Massink & Gethin Norman Editor, editor/s. Ninth Workshop on Quantitative Aspects of Programming Languages (QAPL 2011); Saarbrücken, Germany. Open Publishing Association; 2011-07-04. 61-73. https://doi.org/10.4204/EPTCS.57.5



Loading citation data...

Citation counts
(Requires subscription to view)