Preliminary Report. Final version to appear in: Proceedings QAPL 2011 \begin{matrix}c \\ ◯ \end{matrix} Y. Deng, R.J. van Glabbeek, M. Hennessy & C.C. Morgan This work is licensed under the Creative Commons Attribution License.

Real-Reward Testing for Probabilistic Processes

(Extended Abstract)

Yuxin Deng^{1}^{∗} Rob van Glabbeek^{2} Matthew Hennessy^{3}^{†} Carroll Morgan^{4}^{‡}

1 Shanghai Jiao Tong University and Chinese Academy of Sciences, China 2 National ICT Australia, Australia 3 Trinity College Dublin, Ireland 2,4 University of New South Wales, Australia

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.

1 Introduction

Extending classical testing semantics [1, 7] to a setting in which probability and nondeterminism co-exist was initiated in [13]. The application of a test to a process yields a set of probabilities for reaching a success state. Reward testing was introduced in [8]; here the success states are labelled by nonnegative real numbers—rewards—to indicate degrees of success, and reaching a success state accumulates the associated reward. In [12] an infinite set of success actions is used to report success, and the testing outcomes are vectors of probabilities of performing these success actions. Compared to [8] this amounts to distinguishing different qualities of success, rather than different quantities.

In [13] and [12], both tests and testees are nondeterministic probabilistic processes, whereas [8] allows nonprobabilistic tests only, thereby obtaining a less discriminating form of testing. In [6] we strengthened reward testing by also allowing probabilistic tests. Taking rewards testing in this form we showed that for finitary processes, i.e. finite-state and finitely branching processes, all three modes of testing lead to the same testing preorders. Thus, vector-based testing is no more powerful than scalar testing that employs only one success action, and likewise reward testing is no more powerful than the special case of reward testing in which all rewards are 1. ^{1}

∗Deng was supported by the National Natural Science Foundation of China (61033002).

†Supported by SFI project SFI 06 IN.1 1898.

‡Morgan acknowledges the support of ARC Discovery Grant DP0879529.

1In spite of this there is a difference in power between the notions of testing from [13] and [12], but this is an issue that is entirely orthogonal to the distinction between scalar testing, reward testing and vector-based testing. In [12] it is the execution of a success action that constitutes success, whereas in [1, 7, 13, 8] it is reaching a success state (even though typically success actions are used to identify those states). In [2, Ex 5.3] we showed that state-based testing is (slightly) more powerful than action-based testing. The results presented in [6] about the coincidence of scalar, reward, and vector-based testing preorders pertain to action-based version of each, but in the conclusion it is observed that the same coincidence could be obtained for their state-based versions. In the current paper we stick to state-based testing.

Figure 1: Two processes with divergence and a test

In certain situations it is natural to introduce negative rewards. This is the case, for instance, in the theory of Markov Decision Processes [9]. Intuitively, we could understand negative rewards as costs, while positive rewards are often viewed as benefits or profits. This leads to the question: if negative rewards are also allowed, how would the original reward-testing semantics change? We refer to the more relaxed form of testing, using positive and negative rewards, as real-reward testing and the original one (from [8], but with probabilistic tests as in [6]) as nonnegative-reward testing.

The power of real-reward testing is illustrated in Figure 1. The two (nonprobabilistic) processes in the left- and central diagrams are equivalent under (probabilistic) may- as well as must testing; the τ-loops in the initial states cause both processes to fail any nontrivial must test. Yet, if a reward of −1 is associated with performing the action a, and a reward of 2 with the subsequent performance of b (implemented by the test in the right diagram; see Example 3.8 for more details), in the first process the net reward is either 0 (if the process remains stuck in its initial state) or positive, whereas running the second process may yield a loss. This example shows that for processes that may exhibit divergence, real-reward testing is more discriminating than nonnegative-reward testing, or other forms of probabilistic testing. It also illustrates that the extra power may be relevant in applications.

As remarked, in [6] we established that for finitary processes the nonnegative-reward must-testing preorder (⊑ _{nrmust}) coincides with the probabilistic must-testing preorder (⊑ _{pmust}), and likewise for the may preorders. Here we show that, in contrast to the situation for nonnegative-reward (or scalar) testing, for real-reward testing the may- and must preorders are the inverse of each other, i.e. for any processes Δ and Γ,

Δ ⊑ _{rrmay} Γ iff Γ ⊑ _{rrmust} Δ.  (1)

Our main result is that restricted to finitary convergent processes, the real-reward must preorder coincides with the nonnegative-reward must preorder, i.e. for any finitary convergent processes Δ, Γ,

Δ ⊑ _{rrmust} Γ iff Δ ⊑ _{nrmust} Γ.  (2)

Here by convergence we mean that there is no infinite sequence of internal transitions of the form Λ_{0} −→^{τ} Λ_{1} −→^{τ} ···with distribution Λ_{0} (and thus its successors) reachable from either Δ or Γ. This rules out the processes of Figure 1. Although it is easy to see that in (2) the former implies the latter, to prove the opposite is far from trivial. We employ a novel characterisation of the usual resolution-based testing approach, without introducing concepts like policy [9], adversary [10], scheduler [11] or resolution [6] that are external to the process under investigation; instead we describe the mechanism for gathering test

(⊑ _{rrmay} )^{−1} =^{Thm. 3.7} ⊑ _{rrmust} =^{Thm. 5.6} ⊑ _{nrmust} =^{[6]} ⊑ _{pmust} =^{[3]} ⊑_{FS}

The symbol = between two relations means that they coincide for finitary convergent processes.

Figure 2: The relationship of different testing preorders.

results in terms of the weak τ-moves or derivations [3] the investigated process can make, and hence speak of derivation-based testing.

This allows us to exploit the failure simulation preorder ⊑_{FS} that in [3] was proven to coincide with the probabilistic must testing preorder ⊑ _{pmust} based on resolutions, at least for finitary processes. Using the derivational characterisation we can show that, for finitary convergent processes, ⊑_{FS} is contained in ⊑ _{rrmust} . Convergence is essential here, even though it is not needed to establish that ⊑_{FS} is contained in ⊑ _{nrmust}. Combining this with the results from [6] and [3] mentioned above leads to our required result that ⊑ _{nrmust} is included in ⊑ _{rrmust} , as far as finitary convergent processes are concerned. Consequently, in this case, all the relations of Figure 2 collapse into one.

The rest of this paper is organised as follows. We start by recalling notation for probabilistic labelled transition systems. In Section 3 we review the resolution-based testing approach and show that the realreward may preorder is simply the inverse of the real-reward must preorder. Moreover, using the example of Figure 1, we show that in the presence of divergence the inclusion of ⊑ _{nrmust} in ⊑ _{rrmust} is proper. In Section 4 we present the derivation-based testing approach and also show that the two approaches agree. Then in Section 5 we show for finitary convergent processes that real-reward must testing coincides with nonnegative-reward must testing. We conclude in Section 6.

Due to lack of space, we omit all proofs: they are reported in [4]. Besides the related work already mentioned above, many other studies on probabilistic testing and simulation semantics have appeared in the literature. They are reviewed in [5, 2].

2 Probabilistic Processes

A (discrete) probability subdistribution over a set S is a function Δ : S → [0,1] with ∑_{s∈ S}Δ(s) ≤ 1; the support of such a Δ is ⌈Δ⌉:= {s∈ S | Δ(s) > 0}, and its mass |Δ| is ∑_{s∈⌈Δ⌉}Δ(s). A subdistribution is a (total, or full) distribution if |Δ| = 1. The point distribution \overline{s} assigns probability 1 to s and 0 to all other elements of S, so that ⌈\overline{s}⌉ = \{s\}. With D_{sub}(S) we denote the set of subdistributions over S, and with D(S) its subset of full distributions.

Let {Δ_{k} | k ∈ K} be a set of subdistributions, possibly infinite. Then ∑_{k∈K}Δ_{k} is the real-valued function in S → ℝ defined by (∑_{k∈K}Δ_{k})(s) := ∑_{k∈K}Δ_{k}(s). This is a partial operation on subdistributions because for some state s the sum of Δ_{k}(s) might exceed 1. If the index set is finite, say {1..n}, we often write Δ_{1} + ...+ Δ_{n}. For p a real number from [0,1] we use p·Δ to denote the subdistribution given by (p·Δ)(s) := p·Δ(s). Finally we use ε to denote the everywhere-zero subdistribution that thus has empty support. These operations on subdistributions do not readily adapt themselves to distributions; yet if ∑_{k∈K}p_{k}= 1 for some p_{k} ≥ 0, and the Δ_{k} are distributions, then so is ∑_{k∈K}p_{k}·Δ_{k}.

The expected value ∑_{s∈S} Δ(s)·f(s) over a subdistribution Δ of a bounded nonnegative function f to the reals or tuples of them is written Exp_{Δ}(f), and the image of a subdistribution Δ through a function f : S → T, for some set T, is written Img_{f} (Δ) — the latter is the subdistribution over T given by Img_{f} (Δ)(t) := ∑_{f(s)=t} Δ(s) for each t ∈ T.

Definition 2.1 A probabilistic labelled transition system (pLTS) is a triple ⟨S,Act,→⟩, where

(i) S is a set of states, (ii) Act is a set of visible actions, (iii) relation → is a subset of S × Act_{τ} × D(S). Here Act_{τ} denotes Act ∪ {τ}, where τ ∉ Act is the invisible- or internal action. A (nonprobabilistic) labelled transition system (LTS) may be viewed as a degenerate pLTS — one in which only point distributions are used. In this paper a (probabilistic) process will simply be a distribution over the state set of a pLTS. As with LTSs, we write s −→^{α} Δ for (s,α,Δ)∈ →, as well as s −→^{α} for ∃Δ : s −→^{α} Δ and s → for ∃α: s −→^{α} , with s −̸→^{α} and s ↛ representing their negations. A pLTS is deterministic if for any state s and label α there is at most one distribution Δ with s −→^{α} Δ. It is finitely branching if the set {Δ | s −→^{α} Δ, α ∈ L } is finite for all states s; if moreover S is finite, then the pLTS is finitary. A subdistribution Δ over the state set S of an arbitrary pLTS is finitary if restricting S to the states reachable from Δ yields a finitary sub-pLTS.

3 Testing probabilistic processes

A test is a distribution over the state set of a pLTS having Act_{τ}∪Ω as its set of transition labels, where Ω is a set of fresh success actions, not already in Act_{τ}, introduced specifically to report testing outcomes.^{2} For simplicity we may assume a fixed pLTS of processes—our results apply to any choice of such a pLTS—and a fixed pLTS of tests. Since the power of testing depends on the expressivity of the pLTS of tests—in particular certain types of tests are necessary for our results—let us just postulate that this pLTS is sufficiently expressive for our purposes — for example that it can be used to interpret all processes from the language pCSP, as in our previous papers [5, 2, 3].

Although we use success actions, they are used merely to mark certain states as success states, namely the sources of transitions labelled by success actions. For this reason we systematically ignore the distributions that can be reached after a success action. We impose two requirements on all states in a pLTS of tests, namely

(A) if t −→^{ω_{1}} and t −→^{ω_{2}} with ω_{1},ω_{2} ∈ Ω then ω_{1} = ω_{2}.

(B) if t −→^{ω} with ω ∈ Ω and t −→^{α} Δ with α ∈ Act_{τ} then u −→^{ω} for all u ∈ ⌈Δ⌉. The first condition says that a success state can have one success identity only, whereas the second condition is slight weakening of the requirement from [8] that success states must be end states; it allows further progress from an ω-success state, for some ω ∈ Ω, but ω must remain enabled. ^{3}

To apply test Θ to process Δ we form a parallel composition Θ∥Δ in which all visible actions of Δ must synchronise with Θ. The synchronisations are immediately renamed into τ. The resulting composition is a process whose only possible actions are the elements of Ω_{τ}:= Ω∪{τ}. Formally, if ⟨P,Act,→_{P}⟩ and ⟨T,Act ∪ Ω,→_{T}⟩ are the pLTSs of processes and tests, then the pLTS of applications of tests to processes is ⟨C,Ω,→⟩, with C = {t∥p | t ∈ T∧p∈ P} and → the transition relation generated by the rules in Fig. 3. Here if Θ ∈ D(T) and Δ ∈ D(P), then Θ∥Δ is the distribution given by (Θ∥Δ)(t∥p) := Θ(t)·Δ(p). The resulting pLTS also satisfies (A), (B) above; this would not be the case if we had strengthened (B) to require that success states must be end states.

We will define the result A (Θ,Δ) of applying the test Θ to the process Δ to be a set of testing outcomes, exactly one of which results from each resolution of the choices in Θ∥Δ. Each testing outcome

2For vector-based testing we normally take Ω to be countably infinite [12]. This way we have an unbounded supply of success actions for building tests, of course without obligation to use them all. Scalar testing is obtained by taking |Ω| = 1.

3Justification for imposing such restrictions can be found in Appendix A of [6].

\frac{t −→^{α} _{T} Θ  α ∉ Act}{t∥p −→^{α} Θ∥\overline{p}}  \frac{p −→^{α} _{P} Δ  α ∉ Act}{t∥p −→^{α} \overline{t}∥Δ}  \frac{t −→^{a} _{T} Θ p −→^{a} _{P} Δ a∈ Act}{t∥p −→^{τ} Θ∥Δ}

Figure 3: Synchronous parallel composition between tests and processes

is an Ω-tuple of real numbers in the interval [0,1], i.e. a function o : Ω → [0,1], and its ω-component o(ω), for ω ∈ Ω, gives the probability that the resolution in question will reach an ω-success state, one in which the success action ω is possible.

Due to the presence of nondeterminism in pLTSs, we need a mechanism to reduce a nondeterministic structure into a set of deterministic structures, each of which determines a single possible outcome. Here we adapt the notion of resolution, defined in [6] for probabilistic automata, to pLTSs.

Definition 3.1 [Resolution] A resolution of a subdistribution Δ∈ D_{sub}(S) in a pLTS ⟨S,Ω,→⟩ is a triple ⟨R,Λ,→_{R}⟩ where ⟨R,Ω,→_{R}⟩ is a deterministic pLTS and Λ∈ D_{sub}(R), such that there exists a resolving function f : R → S satisfying

(i) Img_{f} (Λ) = Δ

(ii) if r −→^{α} _{R}Λ′for α ∈ Ω_{τ} then f(r) −→^{α} Img_{f} (Λ′)

(iii) if f(r) −→^{α} for α ∈ Ω_{τ} then r −→^{α} _{R}.

The reader is referred to Section 2 of [6] for a detailed discussion of the concept of resolution, and the manner in which a resolution represents a run of a process; in particular in a resolution states in S are allowed to be resolved into distributions, and computation steps can be probabilistically interpolated. Our resolutions match the results of applying a scheduler as defined in [11].

We now explain how to associate an outcome with a particular resolution, which in turn will associate a set of outcomes with a subdistribution in a pLTS. Given a deterministic pLTS ⟨R,Ω,→_{R}⟩ consider the functional R : (R → [0,1]^{Ω} ) → (R → [0,1]^{Ω} ) defined by

R(f)(r)(ω) := \{ \begin{matrix}1 & if r −→^{ω} \\ 0 & if r −̸→^{ω} and r −̸→^{τ} \\ Exp_{Δ}(f)(ω) & if r −̸→^{ω} and r −→^{τ} Δ. \end{matrix}  (3)

We view the unit interval [0,1] ordered in the standard manner as a complete lattice; this induces the structure of a complete lattice on the product [0,1]^{Ω} and in turn on the set of functions R → [0,1]^{Ω} . The functional R is easily seen to be monotonic and therefore has a least fixed point, which we denote by 𝕍_{⟨R,Ω,→_{R}⟩} ; this is abbreviated to 𝕍 when the deterministic pLTS in question is understood.

Now we define A (Θ,Δ) to be the set of vectors

A (Θ,Δ) := {Exp_{Λ}(𝕍_{⟨R,Ω,→_{R}⟩} ) | ⟨R,Λ,→_{R}⟩ is a resolution of Θ∥Δ} .  (4)

Example 3.2 Consider the process \overline{q_{1}} depicted in Figure 4(a). Here states are represented by filled nodes • and distributions by open nodes ∘. We leave out point-distributions — diverting an incoming edge to the unique state in its support. When we apply the test \overline{t}depicted in Figure 4(b) to it we get the process \overline{t∥q_{1}} depicted in Figure 4(c). This process is already deterministic, hence has essentially only one resolution: itself. Moreover the outcome Exp\overline{t∥q_{1}}(𝕍) = 𝕍(t∥q_{1}) associated with it is the least solution of the equation 𝕍(t∥q_{1}) = \frac{1}{2} · 𝕍(t∥q_{1}) + \frac{1}{2} \overrightarrow{ω} where \overrightarrow{ω} : Ω → [0,1] is the Ω-tuple with \overrightarrow{ω} (ω) = 1 and \overrightarrow{ω} (ω′) = 0 for all ω′≠ ω. In fact this equation has a unique solution in [0,1]^{Ω} , namely \overrightarrow{ω} . Thus A (\overline{t},\overline{q_{1}}) = \{\overrightarrow{ω} \}. □

Figure 4: Testing the process \overline{q_{1}}

Figure 5: Testing the process \overline{q_{2}}

Example 3.3 Consider the process \overline{q_{2}} and the application of the test \overline{t} to it, as outlined in Figure 5. For each k ≥ 1 the process \overline{t∥q_{2}}has a resolution ⟨R_{k},Λ,→_{R_{k}}⟩ such that Exp_{Λ}(𝕍) = (1−\frac{1}{2^{k}})\overrightarrow{ω} ; intuitively it goes around the loop (k − 1) times before at last taking the right hand τ action. Thus A (\overline{t},\overline{q_{2}}) contains (1 − \frac{1}{2^{k}})\overrightarrow{ω} for every k ≥ 1. But it also contains \overrightarrow{ω} , because of the resolution which takes the left hand τ-move every time. Thus A (\overline{t},\overline{q_{2}}) includes the set

\{(1−\frac{1}{2})\overrightarrow{ω} , (1−\frac{1}{2^{2}})\overrightarrow{ω} ,...,(1−\frac{1}{2^{k}})\overrightarrow{ω} ,...,\overrightarrow{ω} \}

As resolutions allow any interpolation between the two τ-transitions from state s_{1}, A (\overline{t},\overline{q_{2}}) is actually the convex closure of the above set. □ There are two standard methods for comparing two sets of ordered outcomes:

O_{1} ≤_{Ho} O_{2} if for every o_{1} ∈ O_{1} there exists some o_{2} ∈ O_{2} such that o_{1} ≤ o_{2}
O_{1} ≤_{Sm} O_{2} if for every o_{2} ∈ O_{2} there exists some o_{1} ∈ O_{1} such that o_{1} ≤ o_{2}

This gives us our definition of the probabilistic may- and must-testing preorders; they are decorated with ·^{Ω} for the repertoire Ω of testing actions they employ.

Definition 3.4 [Probabilistic testing preorders]

(i) Δ ⊑ _{pmay}^{Ω} Γ if for every Ω-test Θ, A (Θ,Δ) ≤_{Ho} A (Θ,Γ). (ii) Δ ⊑ _{pmust}^{Ω} Γ if for every Ω-test Θ, A (Θ,Δ) ≤_{Sm} A (Θ,Γ). These preorders are abbreviated to Δ ⊑ _{pmay} Γ and Δ ⊑ _{pmust} Γ when |Ω| = 1.

In [6] we established that for finitary processes ⊑ _{pmay}^{Ω} coincides with ⊑ _{pmay} and ⊑ _{pmust}^{Ω} with ⊑ _{pmust} for any choice of Ω. We also defined the reward testing preorders in terms of the mechanism set up so far. The idea is to associate with each success action ω ∈ Ω a reward, which is a nonnegative number in the unit interval [0,1]; and then a run of a probabilistic process in parallel with a test yields an expected reward accumulated by those states which can enable success actions. A reward tuple h ∈ [0,1]^{Ω} is used to assign reward h(ω) to success action ω, for each ω ∈ Ω. Due to the presence of nondeterminism, the application of a test Θ to a process Δ produces a set of expected rewards. Two sets of rewards can be compared by examining their suprema/infima; this gives us two methods of testing called reward may/must testing. In [6] all rewards are required to be nonnegative, so we refer to that approach of testing as nonnegative-reward testing. If we also allow negative rewards, which intuitively can be understood as costs, then we obtain an approach of testing called real-reward testing. Technically, we simply let reward tuples h range over the set [−1,1]^{Ω} . If o ∈ [0,1]^{Ω} , we use the dot-product h · o = ∑_{ω∈Ω} h(ω) · o(ω). It can apply to a set O ⊆ [0,1]^{Ω} so that h · O = {h · o | o ∈ O}. Let A ⊆ [−1,1]. We use the notation ⨆ A for the supremum of set A, and ⨅A for the infimum. Definition 3.5 [Reward testing preorders]

(i) Δ ⊑ _{nrmay}^{Ω} Γ if for every Ω-test Θ and nonnegative-reward tuple h ∈ [0,1]^{Ω} , ⨆ h · A (Θ,Δ) ≤ ⨆ h · A (Θ,Γ).

(ii) Δ ⊑ _{nrmust}^{Ω} Γ if for every Ω-test Θ and nonnegative-reward tuple h ∈ [0,1]^{Ω} ,

⨅h · A (Θ,Δ) ≤ ⨅h · A (Θ,Γ). (iii) Δ ⊑ _{rrmay}^{Ω} Γ if for every Ω-test Θ and real-reward tuple h ∈ [−1,1]^{Ω} ,

⨆ h · A (Θ,Δ) ≤ ⨆ h · A (Θ,Γ). (iv) Δ ⊑ _{rrmust}^{Ω} Γ if for every Ω-test Θ and real-reward tuple h ∈ [−1,1]^{Ω} ,

⨅h · A (Θ,Δ) ≤ ⨅h · A (Θ,Γ). This time we drop the superscript Ω iff Ω is countably infinite. It is shown in Corollary 1 of [6] that nonnegative-reward testing is equally powerful as probabilistic testing. Theorem 3.6 [6] For any finitary processes Δ and Γ,

(i) Δ ⊑ _{nrmay} Γ if and only if Δ ⊑ _{pmay} Γ. (ii) Δ ⊑ _{nrmust} Γ if and only if Δ ⊑ _{pmust} Γ. In this paper we focus on the real-reward testing preorders ⊑ _{rrmay} and ⊑ _{rrmust} , by comparing them with the nonnegative reward testing preorders ⊑ _{nrmay} and ⊑ _{nrmust}. Although these two nonnegative-reward testing preorders are in general incomparable we have:

Theorem 3.7 For any processes Δ and Γ, it holds that Δ ⊑ _{rrmay} Γ if and only if Γ ⊑ _{rrmust} Δ.

Our next task is to compare ⊑ _{rrmust} with ⊑ _{nrmust}. The former is included in the latter, which directly follows from Definition 3.5. Surprisingly, it turns out that for finitary convergent processes the latter is also included in the former, thus establishing that the two preorders are in fact the same. The rest of the paper is devoted to proving this result. However, we first show that this result does not extend to divergent processes.

Example 3.8 Consider the processes \overline{q_{1}} and \overline{q_{2}} depicted in Figure 1. Using the characterisations of ⊑ _{pmay} and ⊑ _{pmust} in [3], it is easy to see that these processes cannot be distinguished by probabilistic may- and must testing, and hence not by nonnegative-reward testing either. However, let \overline{t}be the test in the right diagram of Figure 1 that first synchronises on the action a, and then with probability \frac{1}{2} reaches a state in which a reward of −2 is allocated, and with the remaining probability \frac{1}{2} synchronises with the action b and reaches a state that yields a reward of 4. Thus the test employs two success actions ω_{1} and ω_{2}, and we use the reward tuple h with h(ω_{1}) = −2 and h(ω_{2}) = 4. Then the resolution of \overline{q_{1}} that does not involve the τ-loop contributes the value −2 · \frac{1}{2} + 4 · \frac{1}{2} = −1 + 2 = 1 to the set h · A (\overline{t},\overline{q_{1}}), whereas the resolution that only involves the τ-loop contributes the value 0. Due to interpolation, h · A (\overline{t},\overline{q_{1}}) is in fact the entire interval [0,1]. On the other hand, the resolution corresponding to the a-branch of q_{2} contributes the value −1 and h · A (\overline{t},\overline{q_{2}}) = [−1,1]. Thus ⨅h · A (\overline{t},\overline{q_{1}}) = 0 > −1 = ⨅h · A (\overline{t},\overline{q_{2}}), and hence \overline{q_{1}} ⋢ _{rrmust} \overline{q_{2}}. □

4 Derivation-based testing

In this section we give an alternative definition of A (Θ,Δ). Our definition has four ingredients. First of all, for technical reasons we normalise our pLTS of applications of tests to processes by pruning away all outgoing τ-transitions from success states. This way an ω-success state will only have outgoing transitions labelled ω.

Definition 4.1 [ω-respecting] A pLTS ⟨S,Ω,→⟩ is said to be ω-respecting whenever s −→^{ω} , for any ω ∈ Ω, implies s −̸→^{τ} .

It is straightforward to modify the pLTS of applications of tests to processes into one that it is ωrespecting, namely by removing all transitions s −→^{τ} Δ for states s with s −→^{ω} . With [Θ∥Δ] we denote the distribution Θ∥Δ in this pruned pLTS.

Secondly, we recall the definition of weak derivations from [3]. In a pLTS actions are only performed by states, in that actions are given by relations from states to distributions. But processes in general correspond to distributions over states, so in order to define what it means for a process to perform an action, we need to lift these relations so that they also apply to distributions. In fact we will find it convenient to lift them to subdistributions.

Definition 4.2 Let (S,L,→) be a pLTS and R ⊆ S×D_{sub}(S) be a relation from states to subdistributions. Then \overline{R} ⊆ D_{sub}(S) × D_{sub}(S) is the smallest relation that satisfies:

(i) s R Δ implies \overline{s} \overline{R} Δ, and

(ii) (Linearity) Γ_{i} \overline{R} Δ_{i} for i∈ I implies (∑_{i∈I} p_{i}·Γ_{i}) \overline{R} (∑_{i∈I} p_{i}·Δ_{i}) for any p_{i}∈[0,1] (i∈ I) with ∑_{i∈I} p_{i} ≤ 1.

An application of this notion is when the relation is −→^{α} for α ∈ Act_{τ}; in that case we also write −→^{α} for \overline{−→^{α}} . Thus, as source of a relation −→^{α} we now also allow distributions, and even subdistributions. A subtlety of this approach is that for any action α, we have ε −→^{α} ε simply by taking I = ∅ or ∑_{i∈I} p_{i} = 0 in Definition 4.2. That turns out to make ε especially useful for modelling the “chaotic” aspects of divergence in [3], in particular that in the must-case a divergent process can simulate any other.

Definition 4.3 [Weak derivation] Suppose we have subdistributions Δ,Δ\overrightarrow{k} ,Δ_{k}^{×}, for k ≥ 0, with the following properties:

Δ = Δ\overrightarrow{0} + Δ_{0}^{×}
Δ\overrightarrow{0} −→^{τ} Δ\overrightarrow{1} + Δ_{1}^{×}
⋮
Δ\overrightarrow{k} −→^{τ} Δ\overrightarrow{k+ 1}+ Δ_{k+ 1}^{×} .
⋮

Then we call Δ′:= ∑ _{k=0}^{∞} Δ_{k}^{×} a weak derivative of Δ, and write Δ ⟹ Δ′to mean that Δ can make a weak derivation to its derivative Δ′.

There is always at least one weak derivative of any subdistribution (the subdistribution itself) and there can be many.

Thirdly, we identify a class of special weak derivatives called extreme derivatives.

Definition 4.4 [Extreme derivatives] A state s in a pLTS is called stable if s −̸→^{τ} , and a subdistribution Δ is called stable if every state in its support is stable. We write Δ ⟹ ≻ Δ′whenever Δ ⟹ Δ′and Δ′is stable, and call Δ′an extreme derivative of Δ.

Referring to Definition 4.3, we see this means that in the extreme derivation of Δ′from Δ at every stage a state must move on if it can, so that every stopping component can contain only states which must stop: for s ∈ ⌈Δ\overrightarrow{k} + Δ_{k}^{×} ⌉ we have s ∈ ⌈Δ_{k}^{×} ⌉ if and now also only if s −̸→^{τ} . Moreover if the pLTS is ω-respecting then whenever s ∈ ⌈Δ\overrightarrow{k} ⌉, it is not successful, i.e. s −̸→^{ω} for every ω ∈ Ω.

Lemma 4.5 [Existence of extreme derivatives]

(i) For every subdistribution Δ there exists some (stable) Δ′such that Δ ⟹ ≻ Δ′.

(ii) In a deterministic pLTS if Δ ⟹ ≻ Δ′and Δ ⟹ ≻ Δ′′then Δ′= Δ′′.

Subdistributions are essential here. Consider a state t that has only one transition, a self τ-loop t −→^{τ} \overline{t}. Then it diverges and it has a unique extreme derivative ε, the empty subdistribution. More generally, suppose a subdistribution Δ diverges, that is there is an infinite sequence of internal transitions Δ −→^{τ} Δ_{1} −→^{τ} ...Δ_{k} −→^{τ} ... . Then one extreme derivative of Δ is ε, but it may have others.

The final ingredient in the definition of a set of outcomes of an application of a test to a process is the outcome of a particular extreme derivative. Note that all states s ∈ ⌈Δ⌉ in the support of an extreme derivative either satisfy s −→^{ω} for a unique ω ∈ Ω, or have s↛.

Definition 4.6 [Outcomes] The outcome $Δ ∈ [0,1]^{Ω} of a stable subdistribution Δ is given by $Δ(ω) =

∑ {Δ(s) | s ∈ ⌈Δ⌉, s −→^{ω} }.

Putting all four ingredients together, we arrive at a definition of A^{d}(Θ,Δ):

Definition 4.7 Let Δ be a process and Θ an Ω-test. Then A^{d}(Θ,Δ) = {$Λ | [Θ∥Δ] ⟹ ≻ Λ }.

The role of pruning in the above definition can be seen via the following example.

Example 4.8 Let \overline{p} be a process that first does an a-action, to the point distribution \overline{q}, and then diverges, via the τ-loop q −→^{τ} \overline{q}. Let \overline{t} be the test used in Examples 3.2 and 3.3. Then \overline{t}∥\overline{p} has a unique extreme derivative ε, whereas [\overline{t}∥\overline{p}] has a unique extreme derivative [ω∥q]. Here we give the name ω to the state reachable from \overline{t} with the outgoing ω-transition. The outcome in A^{d}(\overline{t},\overline{p}) shows that process \overline{p} passes test \overline{t}with probability 1, which is what we expect for state-based testing. Without pruning we would get an outcome saying that \overline{p} passes \overline{t}with probability 0. □

As this example is nonprobabilistic, it also illustrates how pruning enables the standard notion of nonprobabilistic testing to be captured by derivation-based testing.

Example 4.9 (Revisiting Example 3.2.) The pLTS in Figure 4(c) is deterministic and unaffected by pruning; from part (ii) of Lemma 4.5 it follows that \overline{t∥q_{1}}has a unique extreme derivative Λ. Moreover Λ can be calculated to be ∑_{k≥1} \frac{1}{2^{k}} · \overline{s_{3}},which simplifies to the distribution \overline{s_{3}}. Therefore, A^{d}(\overline{t},\overline{q_{1}}) = \{$\overline{s_{3}}\} = \{\overrightarrow{ω} \}. □

Example 4.10 (Revisiting Example 3.3.) The application of the test \overline{t} to processes \overline{q_{2}} is outlined in Figure 5(c). Consider any extreme derivative Δ′from s_{0} = [\overline{t}∥\overline{q_{2}}]; note that here again pruning actually has no effect. Using the notation of Definition 4.3, it is clear that Δ_{0}^{×} and Δ\overrightarrow{0} must be ε and \overline{s_{0}} respectively. Similarly, Δ_{1}^{×} and Δ\overrightarrow{1} must be ε and \overline{s_{1}} respectively. But s_{1} is a nondeterministic state, having two possible transitions:

(i) s_{1} −→^{τ} Λ_{0} where Λ_{0} has support \{s_{0},s_{2}\} and assigns each of them the weight \frac{1}{2}

(ii) s_{1} −→^{τ} Λ_{1} where Λ_{1} has the support {s_{3},s_{4}}, again dividing the mass equally among them. So there are many possibilities for Δ_{2}; from Definition 4.3 one sees that in fact Δ_{2} can be of the form

p · Λ_{0}+ (1 − p) · Λ_{1}  (5)

for any choice of p ∈ [0,1].

Let us consider one possibility, an extreme one where p is chosen to be 0; only the transition (ii) above is used. Here Δ\overrightarrow{2} is the subdistribution \frac{1}{2} \overline{s_{4}}, and Δ\overrightarrow{k} = ε whenever k > 2. A simple calculation shows that in this case the extreme derivative generated is Λ_{1}^{e} = \frac{1}{2} \overline{s_{3}}+ \frac{1}{2} \overline{s_{6}} which implies that \frac{1}{2} \overrightarrow{ω} ∈ A^{d}(\overline{t},\overline{q_{2}}).

Another possibility for Δ_{2} is Λ_{0}, corresponding to p = 1 in (5) above. Continuing this derivation leads to Δ_{3} being \frac{1}{2} · \overline{s_{1}}+ \frac{1}{2} · \overline{s_{5}}; thus Δ_{3}^{×} = \frac{1}{2} · \overline{s_{5}} and Δ\overrightarrow{3} = \frac{1}{2} · \overline{s_{1}}. Now in the generation of Δ_{4} from Δ\overrightarrow{3} again we resolve a transition from the nondeterministic state s_{1}, by choosing some arbitrary p ∈ [0,1] in (5). Suppose we choose p = 1 every time, completely ignoring transition (ii) above. Then the extreme derivative generated is

Λ_{0}^{e} = ∑_{k≥1} \frac{1}{2^{k}} · \overline{s_{5}}

which simplifies to the distribution \overline{s_{5}}. This in turn means that \overrightarrow{ω} ∈ A^{d}(\overline{t},\overline{q_{2}}).

We have seen two possible derivations of extreme derivatives from \overline{s_{0}}. But there are many others. In general whenever Δ\overrightarrow{k} is of the form q·\overline{s_{1}} we have to resolve the nondeterminism by choosing a p ∈ [0,1] in (5) above; moreover each such choice is independent. It turns out that every extreme derivative Δ′of \overline{s_{0}} is of the form q · Λ_{0}^{e} + (1−q) · Λ_{1}^{e} for some choice of q ∈ [0,1], which implies that A^{d}(\overline{t},\overline{q_{2}}) is the convex closure of the set \{\frac{1}{2} \overrightarrow{ω} ,\overrightarrow{ω} \}. □

We have now seen two ways of associating sets of outcomes with the application of a test to a process. The first, in Section 3, associates with a test and a process a set of deterministic structures called resolutions, while the second, in this section, uses extreme derivations in which nondeterministic choices are resolved dynamically as the derivation proceeds. We proceed to show that these two approaches give rise to the same outcomes. The key result to this end is

Proposition 4.11 Let Λ be a subdistribution in an ω-respecting deterministic pLTS ⟨R,Ω,→_{R}⟩. If Λ ⟹ ≻ Λ′then Exp_{Λ}(𝕍_{⟨R,Ω,→_{R}⟩} ) = Exp_{Λ′}(𝕍_{⟨R,Ω,→_{R}⟩} ).

To obtain it, we need the crucial property that the evaluation function 𝕍 applied to ω-respecting deterministic pLTSs is continuous (with respect to the standard Euclidean metric).

The next proposition maintains that for each extreme derivative there is a corresponding resolution, and vice versa.

Proposition 4.12 Let Δ be a subdistribution over the state set of a pLTS ⟨S,Ω,→⟩.

(i) Suppose Δ ⟹ ≻ Δ′. Then there is a resolution ⟨R,Λ,→_{R}⟩ of Δ, with resolving function f, such that Λ ⟹ ≻ _{R}Λ′for some Λ′for which Δ′= Img_{f} (Λ′).

(ii) Suppose ⟨R,Λ,→_{R}⟩ is a resolution of a Δ with resolving function f.

Then Λ ⟹ ≻ _{R}Λ′implies Δ ⟹ ≻ Img_{f} (Λ′).

The definitions of outcomes, resolutions and the functional R directly imply that if ⟨R,Λ,→_{R}⟩ is a resolution of a subdistribution Δ∈ D_{sub}(S) in a pLTS ⟨S,Ω,→⟩ , with resolving function f, and Λ′∈ D_{sub}(R) is stable, then Img_{f} (Λ′) is stable and

Exp_{Λ′}(𝕍_{⟨R,Ω,→_{R}⟩} ) = $Λ′= $(Img_{f} (Λ′)).

In combination with Propositions 4.11 and 4.12, this yields:

Corollary 4.13 In an ω-respecting pLTS ⟨S,Ω,→⟩, the following statements hold.

(i) If Δ ⟹ ≻ Δ′then there is a resolution ⟨R,Λ,→_{R}⟩ of Δ such that Exp_{Λ}(𝕍_{⟨R,Ω,→_{R}⟩} ) = $(Δ′).

(ii) For any resolution ⟨R,Λ,→_{R}⟩ of Δ, there exists an extreme derivative Δ′such that Δ ⟹ ≻ Δ′and Exp_{Λ}(𝕍_{⟨R,Ω,→_{R}⟩} ) = $(Δ′).

Together with an argument that pruning does not affect A (Θ,Δ), this proves:

Theorem 4.14 For any test Θ and process Δ we have that A^{d}(Θ,Δ) = A (Θ,Δ).

5 Agreement of nonnegative- and real-reward must testing

In this section we prove the agreement of ⊑ _{nrmust} with ⊑ _{rrmust} for finitary convergent processes, by using failure simulation [3] as a stepping stone. We start with defining the weak action relations ⟹^{α} for α ∈ Act_{τ} and the refusal relations −̸→^{A} for A ⊆ Act that are the key ingredients in the definition of the failure-simulation preorder.

Definition 5.1 Let Δ and its variants be subdistributions in a pLTS ⟨S,Act,→⟩.

• For a ∈ Act write Δ ⟹^{a} Δ′whenever Δ ⟹ Δ^{pre} −→^{a} Δ^{post} ⟹ Δ′, for some Δ^{pre} and Δ^{post}. Extend this to Act_{τ} by allowing as a special case that ⟹^{τ} is simply ⟹ , i.e. including identity (rather than requiring at least one −→^{τ} ).

• For A ⊆ Act and s∈ S write s −̸→^{A} if s −̸→^{α} for every α ∈ A ∪ {τ}; write Δ −̸→^{A} if s −̸→^{A} for every s∈⌈Δ⌉.

• More generally write Δ ⟹ −̸→^{A} if Δ ⟹ Δ^{pre} for some Δ^{pre} such that Δ^{pre} −̸→^{A} .

Definition 5.2 [Failure simulation preorder] Define ⊲_{FS} to be the largest relation in S × D_{sub}(S) such that if s ⊲_{FS} Δ then

(i) whenever \overline{s} ⟹^{α} Γ′, for α ∈ Act_{τ}, then there is a Δ′∈ D_{sub}(S) with Δ ⟹^{α} Δ′and Γ′ \overline{⊲_{FS}} Δ′,

(ii) and whenever \overline{s} ⟹ −̸→^{A} then Δ ⟹ −̸→^{A} .

Any relation R ⊆ S × D_{sub}(S) that satisfies the two clauses above is called a failure simulation. The failure simulation preorder ⊑_{FS} ⊆ D_{sub}(S) × D_{sub}(S) is defined by letting Δ ⊑_{FS} Γ whenever there is a Δ^{♮} with Δ ⟹ Δ^{♮} and Γ \overline{⊲_{FS}} Δ^{♮}.

Note that the simulating process, Δ, occurs at the right of ⊲_{FS}, but at the left of ⊑_{FS}.

The failure simulation preorder is preserved under parallel composition with a test, followed by pruning, and it is sound and complete for probabilistic must testing of finitary processes.

Theorem 5.3 [3] For finitary processes Δ and Γ,

(i) If Δ ⊑_{FS} Γ then for any Ω-test Θ it holds that [Δ∥Θ] ⊑_{FS} [Γ∥Θ].

(ii) Δ ⊑_{FS} Γ if and only if Δ ⊑ _{pmust} Γ.

Because we prune our pLTSs before extracting values from them, we will be concerned mainly with ω-respecting structures. Moreover, we require the pLTSs to be convergent in the sense that there is no wholly divergent state s, i.e. with s ⟹ ε.

Lemma 5.4 Let Δ and Γ be two subdistributions in an ω-respecting convergent pLTS ⟨S,Ω,→⟩. If Δ ⊑_{FS} Γ, then it holds that V (Δ) ⊇ V (Γ). Here V (Δ) denotes {$Δ′| Δ ⟹ ≻ Δ′ }.

This lemma shows that the failure-simulation preorder is a very strong relation in the sense that if Δ is related to Γ by the failure-simulation preorder then the set of outcomes generated by Δ includes the set of outcomes given by Γ. It is mainly due to this strong requirement that we can show that the failure-simulation preorder is sound for the real-reward must-testing preorder. Convergence is a crucial condition in this lemma.

Theorem 5.5 For any finitary convergent processes Δ and Γ, if Δ ⊑_{FS} Γ then we have that Δ ⊑ _{rrmust} Γ.

The proof of the above theorem is subtle. The failure-simulation preorder is defined via weak derivations (cf. Definition 5.2), while the reward must-testing preorder is defined in terms of resolutions (cf. Definition 3.5). Fortunately, we have shown in Corollary 4.14 that we can just as well characterise the reward must-testing preorder in terms of weak derivations. Based on this observation, the proof can be carried out by exploiting Theorem 5.3(i) and Lemma 5.4.

This result does not extend to divergent processes. One witness example is given in Figure 1. A simpler example is as follows. Let Δ be a process that diverges, by performing a τ-loop only, and let Γ be a process that merely performs a single action a. It holds that Δ ⊑_{FS} Γ because Δ ⟹ ε and the empty subdistribution can failure-simulate any processes. However, if we apply the test \overline{t} from Example 3.2 again, and the reward tuple h with h(ω) = −1, then

\begin{matrix}⨅h · A^{d}(\overline{t},Δ) = & ⨅h · \{$ε\} = & ⨅\{0\} = & 0 \\ ⨅h · A^{d}(\overline{t},Γ) = & ⨅h · \{\overrightarrow{ω} \} = & ⨅\{−1 \} = & −1 \end{matrix}

As ⨅h · A^{d}(\overline{t},Δ) ≰ ⨅h · A^{d}(\overline{t},Γ), we see that Δ ⋢ _{rrmust} Γ. Since V ([\overline{t}∥Γ]) = \{\overrightarrow{ω} \} but \overrightarrow{ω} ∉ V ([\overline{t}∥Δ]), this also is a counterexample against an extension of Lemma 5.4 with divergence.

Finally, by combining Theorems 3.6(ii) and 5.3(ii), together with Theorem 5.5, we obtain the main result of the paper which states that, in the absence of divergence, nonnegative-reward must testing is as discriminating as real-reward must testing.

Theorem 5.6 For any finitary convergent processes Δ and Γ, it holds that Δ ⊑ _{rrmust} Γ if and only if Δ ⊑ _{nrmust} Γ.

6 Conclusion

We have studied a notion of real-reward testing which extends the traditional nonnegative-reward testing with negative rewards. It turned out that real-reward may preorder is the inverse of real-reward must Y. Deng, R.J. van Glabbeek, M. Hennessy & C.C. Morgan 13

preorder, and vice versa. More interestingly, for finitary convergent processes, the real-reward must testing preorder coincides with the nonnegative-reward testing preorder. In order to prove this result, we have presented two testing approaches and shown their coincidence, which involved proving some analytic properties such as the continuity of a function for calculating testing outcomes.

Although for finitary convergent processes real-reward must testing is no more powerful than nonnegative-reward must testing, the same does not hold for may testing. This is immediate from our result that (the inverse of) real-reward may testing is as powerful as real-reward must testing, that is known not to hold for nonnegative-reward may- and must testing. Thus, real-reward may testing is strictly more discriminating than nonnegative-reward may testing, even without divergence.

References

[1] R. De Nicola & M. Hennessy (1984): Testing equivalences for processes. Theoretical Computer Science 34, pp. 83–133.

[2] Y. Deng, R.J. van Glabbeek, M. Hennessy & C.C. Morgan (2008): Characterising testing preorders for finite probabilistic processes. Logical Methods in Computer Science 4(4):4.

[3] Y. Deng, R.J. van Glabbeek, M. Hennessy & C.C. Morgan (2009): Testing finitary probabilistic processes. In: Proc. CONCUR’09. LNCS 5710, Springer, pp. 274–288.

[4] Y. Deng, R.J. van Glabbeek, M. Hennessy & C.C. Morgan (2010): Real Reward Testing for Probabilistic Processes. Full version of the current paper. Available at http:// basics. sjtu. edu. cn/~yuxin/

temp/ reward. pdf .

[5] Y. Deng, R.J. van Glabbeek, M. Hennessy, C.C. Morgan & C. Zhang (2007): Remarks on Testing Probabilistic Processes. ENTCS 172, pp. 359–397.

[6] Y. Deng, R.J. van Glabbeek, C.C. Morgan & C. Zhang (2007): Scalar Outcomes Suffice for Finitary Probabilistic Testing. In: Proc. ESOP’07. LNCS 4421, Springer, pp. 363–368.

[7] M. Hennessy (1988): An Algebraic Theory of Processes. MIT Press.

[8] B. Jonsson, C. Ho-Stuart & Wang Yi (1994): Testing and Refinement for Nondeterministic and Probabilistic Processes. In: Proc. FTRTFT’94. LNCS 863, Springer, pp. 418–430.

[9] M. Puterman (1994): Markov Decision Processes. Wiley.

[10] J.J.M.M. Rutten, M.Kwiatkowska, G. Norman & D. Parker (2004): Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems, P. Panangaden and F. van Breugel (eds.). CRM Monograph Series 23, American Mathematical Society.

[11] R. Segala (1995): Modeling and Verification of Randomized Distributed Real-Time Systems. Ph.D. thesis, MIT.

[12] R. Segala (1996): Testing Probabilistic Automata. In: Proc. CONCUR’96. LNCS 1119, Springer, pp. 299– 314.

[13] Wang Yi & K.G. Larsen (1992): Testing Probabilistic and Nondeterministic Processes. In: Proc. PSTV’92. IFIP Transactions C-8, North-Holland, pp. 47–61.