Real-Reward Testing for Probabilistic Processes (Extended Abstract)

TL;DR

This paper extends probabilistic process testing to include real-valued rewards, revealing that under certain conditions, the new and traditional testing preorders coincide, simplifying analysis without external resolution structures.

Contribution

Introduces a real-valued reward testing framework for probabilistic processes and characterizes its properties without external resolution mechanisms.

Findings

May and must preorders are inverses in the new framework.

For convergent processes with finite states, real-reward must-testing matches nonnegative-reward must-testing.

The testing outcome function is shown to be continuous.

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.