Real-Reward Testing for Probabilistic Processes (Extended Abstract)

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish
Title of host publicationProceedings of the Ninth Workshop on Quantitative Aspects of Programming Languages, Saarbrücken, Germany, April 1-3, 2011
EditorsMieke Massink, Gethin Norman
PublisherOpen Publishing Association
Pages61-73
Number of pages13
Volume57
DOIs
Publication statusPublished - 4 Jul 2011
EventThe 9th Workshop on Quantitative Aspects of Programming Languages, 2011 - Saarbrücken, Germany
Duration: 1 Apr 20113 Apr 2011
Conference number: 9
http://www.dcs.gla.ac.uk/qapl11/

Publication series

NameElectronic Proceedings in Theoretical Computer Science
PublisherOpen Publishing Association
Volume57
ISSN (Electronic)2075-2180

Workshop

WorkshopThe 9th Workshop on Quantitative Aspects of Programming Languages, 2011
Abbreviated titleQAPL 2011
Country/TerritoryGermany
CitySaarbrücken
Period1/04/113/04/11
Internet address

Fingerprint

Dive into the research topics of 'Real-Reward Testing for Probabilistic Processes (Extended Abstract)'. Together they form a unique fingerprint.

Cite this