Reward Testing Equivalences for Processes

Rob van Glabbeek

Data61, CSIRO, Sydney, Australia School of Computer Science and Engineering, University of New South Wales, Sydney, Australia

                                       rvg@cs.stanford.edu

May and must testing were introduced by De Nicola and Hennessy to define semantic equivalences on processes. May-testing equivalence exactly captures safety properties, and must-testing equivalence liveness properties. This paper proposes reward testing and shows that the resulting semantic equivalence also captures conditional liveness properties. It is strictly finer than both the may- and must-testing equivalence.

This paper is dedicated to Rocco De Nicola, on the occasion of his 65^{th} birthday. Rocco’s work has been a source of inspiration to my own.

Introduction

The idea behind semantic equivalences ≡ and refinement preorders ⊑ on processes is that P ≡ Q says, essentially, that for practical purposes processes P and Q are equally suitable, i.e. one can be replaced for by the other without untoward side effects. Likewise, P ⊑ Q says that for all practical purposes under consideration, Q is at least as suitable as P, i.e. it will never harm to replace P by Q. To this end, Q must have all relevant good properties that P enjoys. Among the properties that ought to be so preserved, are safety properties, saying that nothing bad will even happen, and liveness properties, saying that something good will happen eventually.

In the setting of the process algebra CCS, refinement preorders ⊑_{may} and ⊑_{must}, and associated semantic equivalences ≡_{may} and ≡_{must}, were proposed by De Nicola & Hennessy in [6]. In [12] I argue that ≡_{may}and ≡_{must}are the coarsest equivalences that enjoy some basic compositionality requirements^{1} and preserve safety and liveness properties, respectively. Yet neither preserves so-called conditional liveness properties. This is illustrated in Figure 1, showing two processes that are identified under both

• τ  c  g  ≡_{may} ≡_{must}  • τ  c  g c

Figure 1: Processes identified by may and must testing, but with different conditional liveness properties

may and must testing. From a practical point of view, the difference between these two processes may be enormous. It could be that the action c comes with a huge cost, that is only worth making when the good action g happens afterwards. Only the right-hand side process is able to incur the cost without any benefits, and for this reason it lacks an important property that the left-hand process has. I call such properties conditional liveness properties. A conditional liveness property says that

under certain conditions something good will eventually happen. This paper introduces a stronger form of testing that preserves conditional liveness properties.

1Namely being congruences for injective renaming and partially synchronous interleaving operators, or equivalently all operators of CSP, or equivalently the CCS operators parallel composition, restriction and relabelling.

1 General setting

It is natural to view the semantics of processes as being determined by their ability to pass tests [6, 17]; processes P_{1} and P_{2} are deemed to be semantically equivalent unless there is a test which can distinguish them. The actual tests used typically represent the ways in which users, or indeed other processes, can interact with P_{i}. This idea can be formulated in the following general testing scenario [9], of which the testing scenarios of [6, 17] are instances. It assumes

• a set of processes ℙ,

• a set of tests 𝕋, which can be applied to processes,

• a set of outcomes 𝕆, the possible results from applying a test to a process, and

• a function Apply : 𝕋 × ℙ → P^{+} (𝕆), representing the possible results of applying a specific test

to a specific process. Here P^{+} (𝕆) denotes the collection of non-empty subsets of 𝕆; so the result of applying a test T to a process P, Apply(T,P), is in general a set of outcomes, representing the fact that the behaviour of processes, and indeed tests, may be nondeterministic.

Moreover, some outcomes are considered better then others; for example the application of a test may simply succeed, or it may fail, with success being better than failure. So one can assume that 𝕆 is endowed with a partial order, in which o_{1} ≤ o_{2} means that o_{2} is a better outcome than o_{1}.

When comparing the result of applying tests to processes one needs to compare subsets of 𝕆. There are two standard approaches to make this comparison, based on viewing these sets as elements of either the Hoare or Smyth powerdomain [16, 1] of 𝕆. For O_{1},O_{2} ∈ P^{+} (𝕆) let

(i) 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} (ii) 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}. Using these two comparison methods one obtains two different semantic preorders for processes:

(i) For P,Q ∈ ℙ let P ⊑_{may} Q if Apply(T,P) ⊑_{Ho} Apply(T,Q) for every test T (ii) Similarly, let P ⊑_{must}Q if Apply(T,P) ⊑_{Sm} Apply(T,Q) for every test T. Note that ⊑_{may}and ⊑_{must}are reflexive and transitive, and hence preorders. I use P ≡_{may}Q and P ≡_{must}Q to denote the associated equivalences.

The terminology may and must refers to the following reformulation of the same idea. Let Pass ⊆ 𝕆 be an upwards-closed subset of 𝕆, i.e. satisfying o′≥ o ∈ Pass ⇒ o′∈ Pass, thought of as the set of outcomes that can be regarded as passing a test. Then one says that a process P may pass a test T with an outcome in Pass, notation “P may Pass T ”, if there is an outcome o ∈ Apply(P,T) with o ∈ Pass, and likewise P must pass a test T with an outcome in Pass, notation “P must Pass T ”, if for all o ∈ Apply(P,T) one has o ∈ Pass. Now

P ⊑_{may}Q iff ∀T ∈ 𝕋 ∀Pass ∈ P^{↑}(𝕆)(P may Pass T ⇒ Q may Pass T)
P ⊑_{must}Q iff ∀T ∈ 𝕋 ∀Pass ∈ P^{↑}(𝕆)(P must Pass T ⇒ Q must Pass T)

where P^{↑}(𝕆) is the set of upwards-closed subsets of 𝕆.

The original theory of testing [6, 17] is obtained by using as the set of outcomes 𝕆 the two-point lattice

⊥⊤

with ⊤ representing the success of a test application, and ⊥ failure.

Table 1: Structural operational semantics of CCS

α.E −→^{α} E (Act)  \frac{E_{j} −→^{α} E′_{j}}{∑_{i∈I} E_{i} −→^{α} E′_{j}} (j ∈ I) (Sum)

\frac{E −→^{α} E′}{E|F −→^{α} E′|F}(Par-l)  \frac{E −→^{a} E′, F −→^{ā} F′}{E|F −→^{τ} E′|F′}_{(Comm)}  \frac{F −→^{α} F′}{E|F −→^{α} E|F′}_{(Par-r)}

\frac{E −→^{α} E′}{E\L −→^{α} E′\L} (α,ᾱ ∉ L) (Res)  \frac{E −→^{α} E′}{E[f] −→^{f(α)} E′[f]}(Rel)  \frac{fix⦇S_{X}:S⦈ −→^{α} E}{fix⦇X:S⦈ −→^{α} E} (Rec)

2 CCS: The Calculus of Communicating Systems

CCS [24] is parametrised with a set C of names; Act := C ._{∪} C̄._{∪} {τ}is the set of actions, where τ is a special internal action and C̄:= {c̄| c ∈ C } is the set of co-names. Complementation is extended to C̄by setting ¯ c̄= c. Below, a ranges over A := C ∪ C̄and α over Act. A relabelling is a function f: C →C; it extends to Act by f(c̄)=\overline{f(c)} and f(τ) := τ. Let X be a set X, Y, … of process variables. The set 𝔼_{CCS} of CCS expressions is the smallest set including:

α.E  for α ∈ Act and E ∈ 𝔼_{CCS}  action prefixing
∑_{i∈I} E_{i} for I an index set and E_{i}∈ 𝔼_{CCS}  choice
E|F  for E,F ∈ 𝔼_{CCS}  parallel composition
E\L  for L ⊆ C and E ∈ 𝔼_{CCS}  restriction
E[f]  for f a relabelling and E ∈ 𝔼_{CCS}  relabelling
X  for X ∈ X  process variable
fix⦇X:S⦈ for S: X ⇀𝔼_{CCS} and X ∈ dom(S) recursion.

The expression ∑_{i∈{1,2}}α_{i}.E_{i} is often written as α_{1}.E_{1}+ α_{2}.E_{2}, ∑_{i∈{1}}α_{i}.E_{i} as α_{1}.E_{1}, and ∑_{i∈∅}α_{i}.E_{i} as 0. Moreover, one abbreviates α.0 by α, and P\{c} by P\c. A partial function S: X ⇀ 𝔼_{CCS} is called a recursive specification, and traditionally written as {Y =^{def} S(Y) | Y ∈ dom(S)} . A CCS expression E is closed if each occurrence of a process variable Y in E lays within a subexpression fix⦇X:S⦈ of E with Y ∈ dom(S); ℙ_{CCS}, ranged over by P,Q,..., denotes the set of closed CCS expressions, or processes.

The semantics of CCS is given by the labelled transition relation → ⊆ ℙ_{CCS}× Act × ℙ_{CCS}, where transitions P −→^{α} Qare derived from the rules of Table 1. Here fix⦇S_{X}:S⦈ denotes the expression S(X) (written S_{X}) with fix⦇Y:S⦈ substituted for each free occurrence of Y, for all Y ∈ dom(S), while renaming bound variables in S_{X} as necessary to avoid name-clashes.

The process α.P performs the action α first and subsequently acts as P. The choice operator ∑_{i∈I} P_{i} may act as any of its arguments P_{i}, depending on which of these processes is able to act at all. The parallel composition P|Q executes an action from P, an action from Q, or in the case where P and Q can perform complementary actions a and ā, the process can perform a synchronisation, resulting in an internal action τ. The restriction operator P\L inhibits execution of the actions from L and their complements. The relabelling P[f] acts like process P with all labels α replaced by f(α). Finally, the rule for recursion says that a recursively defined process fix⦇X:S⦈ behaves exactly as the body S_{X} of the recursive equation X =^{def} S_{X}, but with recursive calls fix⦇Y:S⦈ substituted for the variables Y ∈ dom(S).

3 Classical may and must testing for CCS

Let Act^{ω} := Act ∪ {ω}, where ω ∉ Act is a special action reporting success. A CCS test T ∈ 𝕋_{CCS} is defined just like a CCS process, but with α ranging over Act^{ω}. So a CCS process is a special kind of CCS test, namely one that never performs the action ω. To apply the test T to the process P one runs them in parallel; that is, one runs the combined process T |P—which is itself a CCS test.

Definition 1 A computation π is a finite or infinite sequence T_{0},T_{1},T_{2},... of tests, such that (i) if T_{n} is the final element in the sequence, then T_{n} −→^{τ} Tfor no T, and (ii) otherwise T_{n} −→^{τ} T_{n+1}.

A computation π is successful if it contains a state T with T −→^{ω} T′for some T′.

For T ∈ 𝕋_{CCS}, P ∈ ℙ_{CCS}, let Comp(T,P) be the set of computations whose initial element is T |P. Let Apply(T,P) := {⊤ | ∃ successful π ∈ Comp(T,P)} ∪ {⊥ | ∃ unsuccessful π ∈ Comp(T,P)}.

Using this definition of Apply it follows that P ⊑_{may}Q holds unless there is a test T such that T |P has (that is, is the initial state of) a successful computation but Q has not. Likewise P ⊑_{must}Q holds unless there is a test T such that T |P has only successful computations but Q has not.

4 Dual may and must testing

A liveness property [20] is a property that says that something good will eventually happen. In the context of CCS, any test T can be regarded to specify a liveness property; a process P is defined to have this property iff all computations of T |P are successful. Now P ⊑_{must}Q holds iff all liveness properties T ∈ 𝕋_{CCS} that are enjoyed by P also hold for Q.

A safety property [20] is a property that says that something bad will never happen. When thinking of the special action ω as reporting that something bad has occurred, rather than something good, any test T can also be regarded to specify a safety property; a process P is defined to have this property iff none of the computations of T |P are catastrophic; here catastrophic is simply another word for “successful”, when reversing the connotation of ω. Now Q ⊑_{may}P holds iff all safety properties T ∈ 𝕋_{CCS} that are enjoyed by P also hold for Q.

A labelled transition system (LTS) over a set Act is a pair (ℙ,→) where ℙ is a set of processes or states and → ⊆ ℙ × Act × ℙ a set of transitions. In [12] preorders ⊑_{liveness} and ⊑_{safety} are defined on LTSs. Specialised to the LTS (ℙ_{CCS},→) induced by CCS, ⊑_{liveness} coincides with ⊑_{must}, and ⊑_{safety} is exactly the reverse of ⊑_{may}, in accordance with the reasoning above.

To explain the reversal of ⊑_{may} when dealing with safety properties, I propose a variant of CCS testing where in Definition 1 the word “catastrophic” is used for “successful” and Apply is redefined by

Apply(T,P) := {⊥ | ∃ catastrophic π ∈ Comp(T,P)} ∪ {⊤ | ∃ uncatastrophic π ∈ Comp(T,P)}.

An equivalent alternative to redefining Apply is to simply invert the order between ⊥ and ⊤. Let ⊑_{may}^{dual} and ⊑_{must}^{dual}be the versions of the may- and must-testing preorders obtained from this alternative definition. It follows immediately from the definitions that P ⊑_{may}^{dual}Q iff Q ⊑_{must}P and that P ⊑_{must}^{dual}Q iff Q ⊑_{may}P. Based on this, it may be more accurate to say that ⊑_{safety} coincides with ⊑_{must}^{dual}.

A possibility property [21] is a property that says that something good might eventually happen. A test T can be regarded to specify a possibility property; a process P is defined to have this property iff some computation of T |P is successful. Now P ⊑_{may}Q holds iff all possibility properties T ∈ 𝕋_{CCS} that are enjoyed by P also hold for Q. Lamport argues that “verifying possibility properties tells you nothing interesting about a system” [21]. As an example, consider the following models of coffee machines:

C_{1} := τ  C_{2} := τ.c + τ  C_{3} := τ.c

where c is the act of dispensing coffee. The machine C_{1} surely will not make coffee, C_{2} makes a nondeterministic choice between making coffee or not, and C_{3} surely makes coffee. Under may testing, systems C2 and C_{3} are equivalent—both have the possibility of making coffee—and each of them is better than C_{1}: C_{1} ⊏_{may}C_{2} ≡_{may}C_{3}. The relevance of this indeed is questionable. It takes must testing to formalise that C_{3} is better than C_{2}: only C_{3} guarantees that coffee will eventually be dispensed.

When employing dual testing, the same example applies, but with c denoting a catastrophe. Now C_{1} is safe, whereas C_{2} and C_{3} are not: C_{1} ⊐_{must}^{dual}C_{2} ≡_{must}^{dual}C_{3}. Dual may testing would argue that C_{2} is better than C_{3} because a catastrophe might be avoided. This however, can be deemed a weak argument.

In view of these considerations, I will focus on the preorders ⊑_{must}and ⊑_{must}^{dual}(or ⊑_{safety}). The (dual) may preorders simply arise as their inverses, and hence do not require explicit treatment.

5 Reward testing for CCS

A CCS reward test is defined just like a CCS process, but with α ranging over Act × ℝ, the valued actions. A valued action is an action tagged with a real number, the reward for executing this action. A negative reward can be seen as a penalty. Let 𝕋_{CCS}^{R} be the set of CCS reward tests. The structural operational semantics for CCS reward tests has the following modified rules:

\frac{P −→^{a,r} P′, Q ⟶^{ā,r′} Q′}{P|Q −−−→^{τ,r+r′} P′|Q′}_{(Comm′)}  \frac{P −→^{α,r} P′}{P\L −→^{α,r} P′\L}(α,ᾱ ∉ L) (Res′)  \frac{P −→^{α,r} P′}{P[f] −−−→^{f(α),r} P′[f]}_{(Rel′)}

Thus, in synchronising two actions one reaps the rewards of both. In all other rules of Table 1, α is simply replaced by α,r, with r ∈ ℝ. A valued action α,0 is simply denoted α, so that a CCS process can be seen as a special CCS reward test, namely one in which all rewards are 0. To apply a reward test T to a process P one again runs them in parallel.

Definition 2 A reward computation π is a finite or infinite sequence T_{0},r_{1},T_{1},r_{2},T_{2}... of reward tests, such that (i) if T_{n} is the final element in π, then T_{n} −→^{τ,r} Tfor no r and T, and (ii) otherwise T_{n} −⟶^{τ,r_{n+1}} T_{n+1}.

The reward of a finite computation π ending in T_{n} is ∑ _{i=1}^{n} r_{i}. The reward of an infinite computation T_{0},r_{1},T_{1},r_{2},T_{2}... is

inf_{n→∞} ∑_{i=1}^{n} r_{i} ∈ ℝ ∪ {−∞,∞}.

For T ∈ 𝕋_{CCS}^{R}, P ∈ ℙ_{CCS}, let Comp^{R}(T,P) be the set of reward computations with initial element T |P. Let Apply(T,P) := {reward(π) | π ∈ Comp^{R}(T,P)}.

This defines reward preorders ⊑_{reward}^{may}and ⊑_{reward}^{must}on ℙ_{CCS}. It will turn out that P ⊑_{reward}^{may}Q iff Q ⊑_{reward}^{must}P. As a consequence I will focus on ⊑_{reward}^{must}, and simply call it ⊑_{reward}.

6 Characterising reward testing

Assuming a fixed LTS (ℙ,→), labelled over a set Act = A ._{∪} {τ}, the ternary relation =⇒ ⊆ ℙ×A^{∗}×ℙ is the least relation satisfying

P =⇒^{ϵ} P ,  \frac{P −→^{τ} Q}{P =⇒^{ϵ} Q} ,  \frac{P −→^{a} Q, a ≠ τ}{P =⇒^{a} Q}  and  \frac{P =⇒^{σ} Q =⇒^{ρ} r}{P =⇒^{σρ} r} .

For σ ∈ A^{∗} and ν ∈ A^{∗}∪ A^{∞} write σ ≤ ν for “σ is a prefix of ρ”, i.e. “∃ρ .σρ = ν”.

Definition 3 Let P ∈ ℙ.

• a_{1}a_{2}a_{3}···∈ A^{∞} is an infinite trace of P if there are P_{1},P_{2},... such that P =⇒^{a_{1}} P_{1} =⇒^{a_{2}} P_{2} =⇒^{a_{3}} ··· .

• inf(P) denotes the set of infinite traces of P.

• P diverges, notation P⇑, if there are P_{i} ∈ ℙ for all i > 0 such that P −→^{τ} P_{1} −→^{τ} P_{2} −→^{τ} ··· .

• divergences(P) := {σ ∈ A^{∗} | ∃Q. P =⇒^{σ} Q⇑} is the set of divergence traces of P.

• initials(P) := {α ∈ A | ∃Q. P −→^{α} Q}.

• deadlocks(P) := {σ ∈ A^{∗} | ∃Q. P =⇒^{σ} Q ∧ initials(Q) = ∅} is the set of deadlock traces of P.

• CT(P) := inf(P) ∪ divergences(P) ∪ deadlocks(P) is the set of complete traces of P.

• ptraces(P) := {σ ∈ A^{∗} | ∃Q. P =⇒^{σ} Q} is the set of partial traces of P.

• failures(P) := {⟨σ,X⟩ ∈ A^{∗}× P(A) | ∃Q. P =⇒^{σ} Q ∧ initials(Q) ∩ (X ∪ {τ}) = ∅} .

• failures_{d}(P) := failures(P) ∪ {⟨σ,X⟩ | σ ∈ divergences(P) ∧ X ⊆ A }.

• inf_{d}(P) := inf(P) ∪ {ν ∈ A^{∞} | ∀σ< ν ∃ρ ∈ divergences(P). σ ≤ ρ < ν}.

• divergences_{⊥} (P) := {σρ | σ ∈ divergences(P) ∧ ρ ∈ A^{∗}}.

• inf_{⊥} (P) := inf(P) ∪ {σν | σ ∈ divergences(P) ∧ ν ∈ A^{∞} }.

• failures_{⊥} (P) := failures(P) ∪ {⟨σρ,X⟩ | σ ∈ divergences(P) ∧ ρ ∈ A^{∗}∧ X ⊆ A }.

Note that  ptraces(R) = {σ | ⟨σ,∅⟩ ∈ failures_{d}(R)}  for any R ∈ ℙ.  (*)

A path of a process P ∈ ℙ is an alternating sequence P_{0}α_{1}P_{1}α_{2}P_{2}···of processes/states and actions, starting with a state and either being infinite or ending with a state, such that P_{i} −−→^{α_{i+1}} P_{i+1} for all relevant i. Let l(π) := α_{1}α_{2}···be the sequence of actions in π, and ℓ(π) the same sequence after all τs are removed. Now σ ∈ inf(P)∪divergences(P) iff P has an infinite path π with ℓ(π) = σ. Likewise, σ ∈ ptraces(P) iff P has a finite path π with ℓ(π) = σ. Finally, σ ∈ inf(P) ∪ ptraces(P) iff P has an path π with ℓ(π) = σ.

Any transition P|Q −→^{α} Rderives, through the rules of Table 1, from

• a transition P −→^{α} P′and a state Q, where R = P′|Q,

• two transitions P −→^{a_{1}} P′and Q −→^{ā_{2}} Q′ , where R = P′|Q′,

• or from a state P and a transition Q −→^{α} Q′, where R = P|Q′. This transition/state, transition/transition or state/transition pair is called a decomposition of P|Q −→^{α} R; it need not be unique. Now a decomposition of a path π of P|Q into paths π_{1} and π_{2} of P and Q, respectively, is obtained by decomposing each transition in the path, and concatenating all left-projections into a path of P and all right-projections into a path of Q—notation π ∈ π_{1}|π_{2} [15]. Here it could be that π is infinite, yet either π_{1} or π_{2} (but not both) are finite. Again, decomposition of paths need not be unique.

Theorem 1 Let P,Q ∈ ℙ_{CCS}. Then P ⊑_{reward}Q ⇔ divergences(P) ⊇ divergences(Q) ∧ inf(P) ⊇ inf(Q) ∧ failures_{d}(P) ⊇ failures_{d}(Q).

Proof: Let ⊑_{NDFD} be the preorder defined by: P ⊑_{NDFD} Q iff the right-hand side of Theorem 1 holds.

For σ = a_{1}a_{2}··· a_{n} ∈ A^{∗}, let σ̄.T with T ∈ 𝕋_{CCS}^{R} be the CCS reward test ā_{1}.ā_{2}.··· ā_{1}.T. It starts with performing the complements of the actions in σ, where each of these actions is given a reward 0.

Write α^{r} for (α,r) ∈ Act × ℝ. For ν = a_{1}a_{2}a_{3}···∈ A^{∞}, let ν̄^{r} be the CCS reward test fix⦇X_{0}:S⦈ where S = {X_{i} =^{def} ā_{i+1}^{r} .X_{i+1} | i ≥ 0}. This test simply performs the infinite sequence of complements of the actions in ν, where each of these actions is given a reward r.

“⇒”: Suppose P ⋢_{NDFD} Q.

Case 1: Let σ ∈ divergences(Q) \ divergences(P). Take T := σ̄.τ^{−1} .τ^{1} ∈ 𝕋_{CCS}^{R}. Then T |Q has a computation π with reward(π) < 0, whereas T |P has no such computation. Hence P ⋢_{reward}Q.

Case 2: Let ν ∈ inf(Q) \ inf(P). Take T := ν̄^{−1} ∈ 𝕋_{CCS}^{R}. Then T |Q has a computation π with reward(π) = −∞, whereas T |P has no such computation. Hence P ⋢_{reward}Q.

Case 3: Let ⟨σ,X⟩ ∈ failures_{d}(Q) \ failures_{d}(P). Take T := σ̄.τ^{−1} .∑_{a∈X} a^{1} ∈ 𝕋_{CCS}^{R}. Then T |Q has a computation π with reward(π) < 0, whereas T |P has no such computation. Hence P ⋢_{reward}Q.

“⇐”: Suppose P ⊑_{NDFD} Q. Let T ∈ 𝕋_{CCS}^{R}and r ∈ ℝ be such that ∃π ∈ Comp(T |Q) with reward(π) = r. It suffices to find a π′∈ Comp(T |P) with reward(π′) ≤ r. The computation π can be seen as a path of T |Q in which all actions are τ. Decompose this path into paths π_{1} of T and π_{2} of Q. Note that reward(π) = reward(π_{1}).

Case 1: Let π_{2} be infinite. Then ℓ(π_{2}) ∈ inf(Q) ∪ divergences(Q) ⊆ inf(P) ∪ divergences(P). Thus P has an infinite path π′_{2} with ℓ(π′_{2}) = ℓ(π_{2}). Consequently, T |P has an infinite path π′∈ π_{1}|π′_{2} that is a computation with reward(π′) = r.

Case 2: Let π_{2} be finite and π_{1} be infinite. Then ℓ(π_{1}) ∈ divergences(T) and ℓ(π_{2}) ∈ ptraces(Q) ⊆ ptraces(P). The latter inclusion follows by (*). Thus P has a finite path π′_{2} with ℓ(π′_{2}) = ℓ(π_{2}). Consequently, T |P has an infinite path π′∈ π_{1}|π′_{2} that is a computation with reward(π′) = r.

Case 3: Let π_{1} and π_{2} be finite. Let T′ and Q′ be the last states of π_{1} and π_{2}, respectively. Let X := {a ∈ Act | a^{r} ∈ initials(T′)}. Then τ ∉ X, τ ∉ initials(Q′) and initials(Q′)∩X = ∅. So ⟨ℓ(π_{2}),X⟩ ∈ failures(Q) ⊆ failures_{d}(Q) ⊆ failures_{d}(P). Thus P has either an infinite path π′_{2} with ℓ(π′_{2}) = ℓ(π_{2}) or a finite path π′_{2} with ℓ(π′_{2}) = ℓ(π_{2}) and whose last state P′ satisfies initials(P′) ∩ (X ∪ {τ}) = ∅. Consequently, T |P has a finite or infinite path π′∈ π_{1}|π′_{2} that is a computation with reward(π′) = r. □

7 Weaker notions of reward testing

Finite-penalty reward testing doesn’t allow computations that incur infinitely many penalties. A test T ∈ 𝕋_{CCS}^{R} has finite penalties if each infinite path T α_{1}^{r_{1}}T_{1}α_{2}^{r_{2}}T_{2}···has only finitely many transitions i with r_{i} < 0. Let P ⊑_{fp-reward} Q iff Apply(T,P) ⊑_{Sm} Apply(T,Q) for every finite-penalty reward test T.

Theorem 2 Let P,Q ∈ ℙ_{CCS}. Then P ⊑_{fp-reward} Q ⇔ divergences(P) ⊇ divergences(Q) ∧ inf_{d}(P) ⊇ inf_{d}(Q) ∧ failures_{d}(P) ⊇ failures_{d}(Q).

Proof: Let ⊑_{FDI}^{d} be the preorder defined by: P ⊑_{FDI}^{d} Q iff the right-hand side of Theorem 2 holds.

“⇒”: Suppose P ⋢_{FDI}^{d} Q. Case 1 and 3 proceed exactly as in the proof of Theorem 1, but the proof of Case 2 needs to be revised, as its proof uses a test with infinitely many penalties. So assume

divergences(P) ⊇ divergences(Q) ∧ failures_{d}(P) ⊇ failures_{d}(Q)

and let ν ∈ inf_{d}(Q)\inf_{d}(P). I can rule out the case ∀σ< ν ∃ρ ∈ divergences(q). σ ≤ ρ < ν because then ν ∈ inf_{d}(P), using that divergences(Q) ⊆ divergences(P). So ν ∈ inf(Q). Let ν := ν_{1}ν_{2}, where each ρ ∈ divergences(Q) with ρ < ν satisfies ρ < ν_{1}. Let ν_{2} = b_{1}b_{2}···∈ A^{∞}. Take T := ν̄_{1}.τ^{−1} .fix⦇Y_{0}:S⦈, where S = {Y_{i} =^{def} τ^{1}+ b̄_{i+1}.Y_{i+1} | i ≥ 0}. Then T |Q has a computation π with reward(π) < 0, whereas T |P has no such computation. Hence P ⋢_{fp-reward} Q.

“⇐”: Suppose P ⊑_{FDI}^{d} Q. The proof proceeds just as the one of Theorem 1, except for Case 1.

Case 1: Let π_{2} be infinite. Then ℓ(π_{2}) ∈ inf(Q)∪divergences(Q) ⊆ inf_{d}(P)∪divergences(P). In case ℓ(π_{2}) ∈ inf(P) ∪ divergences(P) the proof concludes as for Theorem 1. So assume that ℓ(π_{2}) ∈ A^{∞} and ∀σ< ℓ(π_{2}) ∃ρ ∈ divergences(P). σ ≤ ρ < ℓ(π_{2}). Then there are prefixes π^{†}, π_{1}^{†} and π_{2}^{†} of π, π_{1} and π_{2} such that (i) π^{†} ∈ π_{1}^{†}|π_{2}^{†} , (ii) there are no negative rewards allocated in the suffix of π_{1} past π_{1}^{†}, and (iii) ℓ(π_{2}^{†}) ∈ divergences(P). Let π′_{2} be an infinite path of P with ℓ(π′_{2}) = ℓ(π_{2}^{†}). Then there is a computation π′∈ π_{1}^{†}|π′_{2} of T |P with reward(π′) = reward(π_{1}^{†}) ≤ reward(π_{1}) = r. □

Single penalty reward testing doesn’t allow computations that incur multiple penalties. A test T ∈ 𝕋_{CCS}^{R}has the single penalty property if each path T α_{1}^{r_{1}}T_{1}α_{2}^{r_{2}}T_{2}···has at most one transition i with r_{i} < 0. Let P ⊑_{sp-reward} Q iff Apply(T,P) ⊑_{Sm} Apply(T,Q) for every single penalty reward test T. Obviously, ⊑_{sp-reward} coincides with ⊑_{fp-reward}. This follows because all test used in the proof of Theorem 2 have the single penalty property.

Analogously one might weaken reward testing and/or single penalty reward testing by requiring that in each computation only finitely many, or at most one, positive reward can be reaped. This does not constitute a real weakening, as the tests used in Theorems 1 and 2 already allot at most a single positive reward per computation only.

Nonnegative reward testing requires all rewards to be nonnegative. Let P ⊑_{+reward} Q iff Apply(T,P) ⊑_{Sm} Apply(T,Q) for every nonnegative reward test T. Likewise ⊑_{−reward} requires all rewards to be 0 or negative.

Theorem 3 Let P,Q ∈ ℙ_{CCS}. Then P ⊑_{+reward} Q ⇔ divergences_{⊥} (P) ⊇ divergences_{⊥} (Q) ∧ inf_{⊥} (P) ⊇ inf_{⊥} (Q) ∧ failures_{⊥} (P) ⊇ failures_{⊥} (Q).

Proof: Let ⊑_{FDI}^{⊥} be the preorder defined by: P ⊑_{FDI}^{⊥} Q iff the right-hand side of Theorem 3 holds.

“⇒”: Suppose P ⋢_{FDI}^{⊥} Q.

Case 1: Let σ = a_{1}a_{2}··· a_{n} ∈ divergences_{⊥} (Q) \ divergences_{⊥} (P). Take T := fix⦇X_{0}:S⦈ in which

S = {X_{i} =^{def} τ^{1}+ a_{i+1} .X_{i+1} | 0≤ i< n} ∪ {X_{n} =^{def} τ^{1}}.

Then T |Q has a computation π with reward(π) < 1, which T |P has not. Hence P ⋢_{+reward} Q.

Case 2: Let ν = a_{1}a_{2}···∈ inf_{⊥} (Q)\inf_{⊥} (P). Let T := fix⦇X_{0}:S⦈ with S = {X_{i−1} =^{def} τ^{1}+ a_{i}.X_{i} | i≥ 1}. Then T |Q has a computation π with reward(π) < 1, which T |P has not. Hence P ⋢_{+reward} Q.

Case 3: Let ⟨a_{1}a_{2}··· a_{n},X⟩ ∈ failures_{⊥} (Q) \ failures_{⊥} (P). Take T := fix⦇X_{0}:S⦈ in which

S = {X_{i} =^{def} τ^{1}+ a_{i+1} .X_{i+1} | 0≤ i< n} ∪ {X_{n} =^{def} ∑_{a∈X}a^{1}}.

Then T |Q has a computation π with reward(π) < 1, which T |P has not. Hence P ⋢_{+reward} Q.

“⇐”: Suppose P ⊑_{FDI}^{⊥} Q. Let T ∈ 𝕋_{CCS}^{R} be a nonnegative rewards test and r ∈ ℝ be such that there is a π ∈ Comp(T |Q) with reward(π) = r. It suffices to find a π′∈ Comp(T |P) with reward(π′) ≤ r. The computation π can be seen as a path of T |Q in which all actions are τ. Decompose this path into paths π_{1} of T and π_{2} of Q. Note that reward(π) = reward(π_{1}).

Case 1: Let π_{2} be infinite. Then ℓ(π_{2}) ∈ inf(Q) ∪ divergences(Q) ⊆ inf_{⊥} (P) ∪ divergences_{⊥} (P). If ℓ(π_{2}) ∈ inf(P) ∪ divergences(P) then P has an infinite path π′_{2} with ℓ(π′_{2}) = ℓ(π_{2}). Consequently, T |P has an infinite path π′∈ π_{1}|π′_{2} that is a computation with reward(π′) = r. The alternative is that ℓ(π_{2}) has a prefix in divergences(P). In that case there are prefixes π^{†}, π_{1}^{†} and π_{2}^{†} of π, π_{1} and π_{2} such that π^{†} ∈ π_{1}^{†}|π_{2}^{†} and ℓ(π_{2}^{†}) ∈ divergences(P). Let π′_{2} be an infinite path of P with ℓ(π′_{2}) = ℓ(π_{2}^{†}). Then there is a computation π′∈ π_{1}^{†}|π′_{2} of T |P with reward(π′) = reward(π_{1}^{†}) ≤ reward(π_{1}) = r.

Case 2: Let π_{2} be finite and π_{1} be infinite. Then ℓ(π_{1}) ∈ divergences(T) and ℓ(π_{2}) ∈ ptraces(Q) ⊆ ptraces(P) ∪ divergences_{⊥} (P). The latter inclusion follows since

ptraces(R) ∪ divergences_{⊥} (R) = {σ | ⟨σ,∅⟩ ∈ failures_{⊥} (R)}

for any R ∈ ℙ. If ℓ(π_{2}) ∈ ptraces(P) then P has a finite path π′_{2} with ℓ(π′_{2}) = ℓ(π_{2}). Consequently, T |P has an infinite path π′∈ π_{1}|π′_{2} that is a computation with reward(π′) = r. The alternative is handled just as for Case 1 above.

Case 3: Let π_{1} and π_{2} be finite. Let T′ and Q′ be the last states of π_{1} and π_{2}, respectively. Let X := {a ∈ Act | a^{r} ∈ initials(T′)}. Then τ ∉ X, τ ∉ initials(Q′) and initials(Q′)∩X = ∅. So ⟨ℓ(π_{2}),X⟩ ∈ failures(Q) ⊆ failures_{⊥} (Q) ⊆ failures_{⊥} (P). If ⟨ℓ(π_{2}) ∈ failures(P) then P has a finite path π′_{2}with ℓ(π′_{2}) = ℓ(π_{2}) and whose last state P′ satisfies initials(P′) ∩ (X ∪ {τ}) = ∅. Consequently, T |P has a finite or infinite path π′∈ π_{1}|π′_{2} that is a computation with reward(π′) = r. The alternative is handled just as for Case 1 above. □

One might weaken nonnegative reward testing by requiring that in each computation only finitely many, or at most one, reward can be reaped. This does not constitute a real weakening, as the tests used in Theorem 3 already allot at most a single reward per computation only.

Theorem 4 Let P,Q ∈ ℙ_{CCS}. Then P ⊑_{−reward} Q ⇔ ptraces(P) ⊇ ptraces(Q) ∧ inf(P) ⊇ inf(Q)

Proof: Let ⊑_{T}^{∞} be the preorder defined by: P ⊑_{T}^{∞} Q iff the right-hand side of Theorem 4 holds.

“⇒”: Suppose P ⋢_{T}^{∞} Q.

Case 1: Let σ ∈ ptraces(Q) \ ptraces(P). Take T := σ̄.τ^{−1} . Then T |Q has a computation π with reward(π) < 1, which T |P has not. Hence P ⋢_{−reward} Q.

Case 2 proceeds exactly as in the proof of Theorem 1.

“⇐”: Suppose P ⊑_{T}^{∞} Q. Let T ∈ 𝕋_{CCS}^{R} be a nonpositive rewards test and r ∈ ℝ be such that there is a π ∈ Comp(T |Q) with reward(π) = r. It suffices to find a π′∈ Comp(T |P) with reward(π′) ≤ r. The computation π can be seen as a path of T |Q in which all actions are τ. Decompose this path into paths π_{1} of T and π_{2} of Q. Note that reward(π) = reward(π_{1}).

Moreover, ℓ(π_{2}) ∈ inf(Q)∪ptraces(Q) ⊆ inf(P)∪ptraces(P). So P has a path π′_{2}with ℓ(π′_{2}) = ℓ(π_{2}). Consequently, T |P has an path π′∈ π_{1}|π′_{2} that is either a computation, or a prefix of a computation, with reward(π′) = r. In case it is a prefix of a computation π′′then reward(π′′) ≤ reward(π′) = r. □

Finite-penalty nonpositive reward testing only allows computations that incur no positive rewards and merely finitely many penalties. Let P ⊑_{fp-−reward} Q iff Apply(T,P) ⊑_{Sm} Apply(T,Q) for every finitepenalty nonpositive reward test T.

Theorem 5 Let P,Q ∈ ℙ_{CCS}. Then P ⊑_{fp-−reward} Q ⇔ ptraces(P) ⊇ ptraces(Q)

Proof: Let ⊑_{T} be the preorder defined by: P ⊑_{T} Q iff the right-hand side of Theorem 5 holds.

“⇒”: Suppose P ⋢_{T} Q. Let σ ∈ ptraces(Q)\ptraces(P). Take T := σ̄.τ^{−1} . Then T |Q has a computation π with reward(π) < 1, which T |P has not. Hence P ⋢_{−reward} Q.

“⇐”: Suppose P ⊑_{T} Q. Let T ∈ 𝕋_{CCS}^{R}be a finite-penalty nonpositive rewards test and r ∈ ℝ be such that there is a π ∈ Comp(T |Q) with reward(π) = r. Then π has a finite prefix π^{†} (not necessarily a computation) with reward(π) = r. It suffices to find a prefix π′of a computation of T |P with reward(π′) = r. The finite prefix π^{†} can be seen as a path of T |Q in which all actions are τ. Decompose this path into finite paths π_{1} of T and π_{2} of Q. Now ℓ(π_{2}) ∈ ptraces(Q) ⊆ ptraces(P). So P has a path π′_{2}with ℓ(π′_{2}) = ℓ(π_{2}). Consequently, T |P has a path π′∈ π_{1}|π′_{2} that is a prefix of a computation, with reward(π′) = r. □

Single penalty nonpositive reward testing only allows computations that incur no positive rewards and at most one penalty. Let P ⊑_{sp-−reward} Q iff Apply(T,P) ⊑_{Sm} Apply(T,Q) for every single penalty nonpositive reward test T. Obviously, ⊑_{sp-−reward} coincides with ⊑_{fp-−reward} . This follows because all test used in the proof of Theorem 5 have the single penalty property.

8 Reward may testing

Call a test T ∈ 𝕋_{CCS}^{R} well-behaved if for each infinite path T α_{1}^{r_{1}}T_{1}α_{2}^{r_{2}}T_{2}···the limit lim_{n→∞} ∑ _{i=1}^{n} r_{i} ∈ ℝ∪{−∞,∞} exists. If the sequence (r_{i})_{i=1}^{∞} alternates between 1 and −1 for instance, the test is not wellbehaved. Since all tests used in the proof of Theorem 1 are well-behaved, the reward testing preorder ⊑_{reward}would not change if one restricts the collection of available test to the well-behaved ones only. When restricting to well-behaved tests, the infimum inf_{n→∞} in Definition 2 may be read as lim_{n→∞} .

Theorem 6 P ⊑_{reward}^{may}Q iff Q ⊑_{reward}^{must}P.

Proof: For any well-behaved test T, let −T be obtained by changing all occurrences of actions (α,r) into (α,−r). Now Apply(−T,P) = {−r |r ∈Apply(T,P)}. This immediately yields the claimed result.□

All weaker notions of testing contemplated in Section 7 employ well-behaved tests only. The same reasoning as above yields (besides ⊑_{reward}^{may} = ⊑_{reward}^{−1})

⊑_{fp-reward}^{may} = ⊑_{reward}^{−1} , ⊑_{+reward}^{may} = ⊑_{−reward}^{−1} , ⊑_{−reward}^{may} = ⊑_{+reward}^{−1} and ⊑_{fp-−reward}^{may} = ⊑_{−reward}^{−1} .

9 A hierarchy of testing preorders

Theorem 7 P ⊑_{must}Q iff P ⊑_{+reward} Q. Likewise, P ⊑_{must}^{dual}Q iff P ⊑_{fp-−reward} Q.

Proof: “If”: Without affecting ⊑_{must}one may restrict attention to tests T ∈ 𝕋_{CCS} with the property that each path of T contains at most one success state—one with an outgoing transition labelled ω. Namely, any outgoing transition of a success state may safely be omitted. Now each such test T can be converted into a nonnegative reward test T′, namely by assigning a reward 1 to any action leading into a success state, keeping the rewards of all other actions 0. The success action itself may then be renamed into τ, or omitted. Now trivially, a computation of T |P is successful iff the matching computation of T′yields a reward 1; a computation of T |P is unsuccessful iff the matching computation of T′yields a reward 0. It follows that must-testing can be emulated by nonnegative reward testing.

“Only if”: As remarked in Section 7, nonnegative reward testing looses no power when allowing only one reward per computation. For the same reasons it looses no power if each positive reward is 1. Now any reward test T′∈ 𝕋_{CCS}^{R} with these restrictions can be converted to a test T ∈ 𝕋_{CCS} by making any target state of a reward-1 transition into a success state. It follows that nonnegative reward testing can be emulated by must-testing.

The second statement follows in the same way, but using a reward −1. □

⊑_{may}^{−1} = ⊑_{must}^{dual} = ⊑_{fp-−reward} = ⊑_{T} = ⊑_{safety} ⊑_{−reward} = ⊑_{T}^{∞} ⊑_{reward} = ⊑_{NDFD} = ⊑_{lt-properties} ⊑_{must} = ⊑_{+reward} = ⊑_{FDI}^{⊥} = ⊑_{liveness} ⊑_{fp-reward} = ⊑_{FDI}^{d} = ⊑_{cond. liveness}

Figure 2: A spectrum of testing preorders

A preorder ⊑_{X} is said to be finer than or equal to a preorder ⊑_{Y}iff P ⊑_{X} Q ⇒ P ⊑_{Y}Q for all P and Q; in that case ⊑_{Y} is coarser than or equal to ⊑_{X}.

Theorem 8 The preorders occurring in this paper are related as indicated in Figure 2, where the arrows point in the coarser direction.

Proof: The relations between ⊑_{reward}, ⊑_{fp-reward}, ⊑_{+reward} , ⊑_{−reward} and ⊑_{fp-−reward} follow immediately from the definitions, as the coarser variant uses only a subset of the tests available to the finer variant. The strictness of all these relations is obtained by the examples below.

The connections with ⊑_{must}, ⊑_{must}^{dual}and the inverse of ⊑_{may}are provided by Theorem 7 and Section 4. The characterisations in terms of ⊑_{NDFD}, ⊑_{FDI}^{d}, ⊑_{FDI}^{⊥}, ⊑_{F}^{∞} and ⊑_{T} are provided by Theorems 1–5. The connections with ⊑_{lt-properties}, ⊑_{cond. liveness}, ⊑_{liveness} and ⊑_{safety} will be established in Section 10. □

Let a^{n}.P be defined by a^{0}.P := P and a^{i+1} .P = a.a^{i}.P. Furthermore, let a^{∞} := fix⦇X:X =^{def} a.X⦈be a process that performs infinitely many as. Let Δ be the unary operator given by ΔP := fix⦇X:X =^{def} τ.X + P ⦈. It first performs 0 or more τ-actions, and if this number is finite subsequently behaves as its argument P. So Δ0 = τ^{∞} just performs an infinite sequence of τ-moves.

Example 1 ∑_{n≥1} a^{n}.Δ0 ≡_{fp-reward} a^{∞} + ∑_{n≥1} a^{n}.Δ0, but ∑_{n≥1} a^{n}.Δ0 ⋢_{−reward} a^{∞} + ∑_{n≥1} a^{n}.Δ0 (and thus ⋢_{reward}).

Example 2 Δ(c.g) ≡_{must}Δ(c + c.g) and Δ(c.g) ≡_{−reward} Δ(c + c.g), yet Δ(c.g) ⋢_{fp-reward} Δ(c + c.g). These are the processes displayed in Figure 1. A test showing the latter is c^{−1}.g^{1}.

Example 3 c.g ≡_{fp-−reward} c + c.g, yet c.g ⋢_{+reward} c + c.g. A test showing the latter is c.g^{1}.

Example 4 Δa ≡_{+reward} Δ0, yet Δa ⋢_{fp-−reward} Δ0. A test showing the latter is a^{−1} .

A process P is divergence-free if divergences(P) = ∅. It is regular, or finite-state, if there only finitely many processes Q such that ∃σ ∈ A^{∗}. P =⇒^{σ} Q. It is =⇒ -image-finite if for each σ ∈ A^{∗} there are only finitely many Q such that P =⇒^{σ} Q. Note that the class of =⇒ -image-finite processes is not closed under parallel composition, or under renaming transition labels a ∈ A into τ. Regular processes are =⇒ -image-finite. Any P ∈ ℙ_{CCS} without parallel composition, relabelling or restriction is regular. Any P ∈ ℙ_{CCS} without recursion is both divergence-free and regular.

Proposition 1 If P ∈ ℙ_{CCS} is divergence-free, then P ⊑_{+reward} Q iff P ⊑_{reward}Q.

Proof: This follows immediately from Theorems 1 and 3, using that divergences(P) = ∅, inf_{⊥} (P) = inf_{d}(P) = inf(P) and failures_{⊥} (P) = failures_{d}(P) = failures(P). (In case Q is not divergence-free one has neither P ⊑_{+reward} Q nor P ⊑_{reward}Q.) □

Proposition 2 If P is =⇒ -image-finite then (a) P ⊑_{fp-−reward} Q iff P ⊑_{−reward} Q and (b) P ⊑_{fp-reward} Q iff P ⊑_{reward}Q.

Proof: By Königs lemma ν ∈ A^{∞} is an infinite trace of P iff only if each finite prefix of ν is a partial trace of P. Now (a) follows immediately from Theorems 4 and 5: Suppose P ⊑_{−reward} Q and ν ∈ inf(Q). Then each finite prefix of ν is in ptraces(Q) and thus in ptraces(P). Thus ν ∈ inf(P).

(b) follows in the same way from Theorems 1 and 2, using (*). □

10 Conditional liveness properties

To obtain a general liveness property for labelled transition systems, assume that some notion of good is defined. Now, to judge whether a process P satisfies this liveness property, one should judge whether P can reach a state in which one would say that something good had happened. But all observable behaviour of P that is recorded in a labelled transition system until one comes to such a verdict, is the sequence of visible actions performed until that point. Thus the liveness property is completely determined by the set sequences of visible actions that, when performed by P, lead to such a judgement. Therefore one can just as well define a liveness property in terms of such a set.

Definition 4 A liveness property of processes in an LTS is given by a set G ⊆ A^{∗}. A process P satisfies this liveness property, notation P ⊧ liveness(G), when each complete trace of P has a prefix in G.

This formalisation of liveness properties stems from [12] and is essentially different from the one in [2] and most subsequent work on liveness properties; this point is discussed in [12, Section 6].

A preorder ⊑ preserves liveness properties if P ⊑ Q implies that Q enjoys any liveness property that P has. It is a precongruence for an n-ary operator op if P_{i} ⊑ Q_{i} for i = 1,...,n implies op(P_{1},...,P_{n}) ⊑ op(Q_{1},...,Q_{n}). Now let ⊑_{liveness} be the coarsest preorder that is a precongruence for the operators of CSP and preserves liveness properties. In [12] it is shown that this preorder exists, and equals ⊑_{F DI}^{⊥}, as defined in the proof of Theorem 3. The proof of this result does not require that ⊑_{liveness} be a preorder for all operators of CSP; it goes through already when merely requiring it to be precongruence for injective renaming and partially synchronous interleaving operators. Looking at this proof, the same can also be obtained requiring ⊑_{liveness} to be a precongruence for the CCS operators |, \L and injective relabelling.

It follows that ⊑_{liveness} coincides with ⊑_{+reward} (cf. Theorem 8). This connection can be illustrated by a translation from liveness properties G ⊆ A^{∗} (w.l.o.g. assumed to have the property that if σ ∈ G then σρ ∉ G for any ρ ≠ ϵ) to nonnegative reward tests T_{G}. Here T_{G} can be rendered as a deterministic tree in which all transitions completing a trace from Ḡ yield a reward 1, so that all computations of T |P earn a positive reward iff P ⊧ liveness(G).

One obtains a general concept of safety property by means of the same argument as for liveness properties above, but using “bad” instead of “good”.

Definition 5 A safety property of processes in an LTS is given by a set B ⊆ A^{∗}. A process P satisfies this safety property, notation P ⊧ safety(B), when ptraces(p) ∩ B = ∅.

This formalisation of safety properties stems from [12] and is in line with the one in [2]. Now let ⊑_{safety} be the coarsest precongruence (for the same choice of operators as above) that preserves safety properties. In [12] it is shown that this preorder exists, and equals ⊑_{T}, as defined in the proof of Theorem 5.

It follows that ⊑_{safety} coincides with ⊑_{fp-−reward} (cf. Theorem 8). This connection can be illustrated by a translation from safety properties B ⊆ A^{∗} (w.l.o.g. assumed to have the property that if σ ∈ B then σρ ∉ B for any ρ ≠ ϵ) to nonnegative reward tests T_{B}. Here T_{B} can be rendered as a deterministic tree in which all transitions completing a trace from B̄yield a reward −1, so that all computations of T |P earn a nonnegative reward iff P ⊧ safety(B).

A conditional liveness property says that under certain conditions something good will eventually happen. To obtain a general conditional liveness property for LTSs, assume that some condition, and some notion of good is defined. Now, to judge whether a process P satisfies this conditional liveness property, one should judge first of all in which states the condition is fulfilled. All observable behaviour of P that is recorded in an LTS until one comes to such a verdict, is the sequence of visible actions performed until that point. Thus the condition is completely determined by the set of sequences of visible actions that, when performed by P, lead to such a judgement. Next one should judge whether P can reach a state in which one would say that something good had happened. Again, this judgement can be expressed in terms of the sequences of visible actions that lead to such a state.

Definition 6 ([12]) A conditional liveness property of processes in an LTS is given by two sets C,G ⊆ A^{∗}. A process P satisfies this conditional liveness property, notation P ⊧ liveness_{C}(G), when each complete trace of P that has a prefix in C, also has a prefix in G.

Now let ⊑_{cond. liveness} be the coarsest precongruence (for the same choice of operators as above) that preserves conditional liveness properties. In [12] it is shown that this preorder exists, and equals ⊑_{F DI}^{d}, as defined in the proof of Theorem 2. It follows that ⊑_{safety} coincides with ⊑_{fp-reward} (cf. Theorem 8).

Similar to the above cases, this connection can be illustrated by a translation from conditional liveness properties C,G ⊆ A^{∗} to reward tests in which each computation has at most one negative and one positive reward, which are always −1 and +1.

Definition 7 A linear time property of processes in an LTS is given by a set Φ ⊆ A^{∗}∪ A^{∞} of finite and infinite sequences of actions. A process P satisfies this property, notation P ⊧ Φ, when CT(P) ⊆ Φ.

A liveness property is a special kind of linear time property:

liveness(G) = {σ ∈ A^{∗}∪ A^{∞} | ∃ρ ∈ G. ρ ≤ σ}.

Likewise, safety(B) = {σ ∈ A^{∗}∪ A^{∞} | ¬∃ρ ∈ B. ρ ≤ σ}, and

liveness_{C}(G) = {σ ∈ A^{∗}∪ A^{∞} | (∃ρ ∈ C. ρ ≤ σ) ⇒ (∃ν ∈ G. ν ≤ σ)}. Now let ⊑_{lt. properties}be the coarsest precongruence (for the same choice of operators as above) that

preserves linear time properties. In [19, 12] it is shown that this preorder exists, and equals ⊑_{NDF D}, as defined in the proof of Theorem 1. It follows that ⊑_{lt. properties} coincides with ⊑_{reward}(cf. Theorem 8).

11 Congruence properties

Theorem 9 The preorders of this paper are precongruences for the CCS operators |, \L and [f].

Proof: Note that Apply(T,R|P) = Apply(T|R,P), using the associativity (up to strong bisimilarity) of |. Therefore P ⊑_{reward}Q implies R|P ⊑_{reward}R|Q, showing that ⊑_{reward} is a precongruence for parallel composition. The same holds for ⊑_{fp-reward}, ⊑_{+reward} , ⊑_{−reward} and ⊑_{fp-−reward} .

Likewise Apply(T,P\L) = Apply(T\L,P). This yields precongruence results for restriction.

Finally, Apply(T,P[f ]) = Apply(T[f^{−1} ],P), yielding precongruence results for relabelling.

Here [f^{−1} ] is an operator with rule \frac{E −→^{α,r} E′}{E[f^{−1} ] −→^{β,r} E′[f^{−1} ]} (f(β) = α). Although this is not a CCS operator,

for any test T the test T [f^{−1} ] is expressible in CCS, on grounds that each process in an LTS is expressible in CCS. □

Theorem 10 The preorders of this paper are precongruences for action prefixing.

Proof: This follows in a straightforward way from the characterisations of the preorders in Sections 6 and 7. For instance, failures_{d}(a.P) = {⟨aσ,X⟩ | ⟨σ,X⟩ ∈ failures_{d}(a.P)}. □

In the same way it follows that ⊑_{fp-−reward} and ⊑_{−reward} are precongruences for the CCS operator +. However, the preorders ⊑_{reward}, ⊑_{fp-reward} and ⊑_{+reward} fail to be congruences for choice:

Example 5 0 ≡_{reward}τ, yet 0 + a ⋢_{+reward} τ + a, using that ⟨ϵ,A ⟩ ∈ failures_{⊥} (τ + a) \ failures_{⊥} (0 + a).

This issue occurs for almost all semantic equivalences and preorders that abstract from internal actions. The standard solution is to replace each such preorder ⊑_{X} by the coarsest precongruence for the operators of CCS that is finer than ⊑_{X}. Let stable be the predicate that holds for a process P iff there is no P′with P −→^{τ} P′. Write P ⊑_{X}^{τ} Q iff P ⊑_{X} Q ∧ (stable(P) ⇒ stable(Q)).

Theorem 11 Let X ∈ {reward, fp-reward, +reward}. Then ⊑_{X}^{τ} is the coarsest precongruence for the operators of CCS that is contained in ⊑_{X}.

Proof: That ⊑_{+reward}^{τ} is a precongruence for + follows with Theorem 3 since

stable(P + Q) ⇔ stable(P) ∧ stable(Q)
failures_{⊥} (P + Q) = {⟨σ,X⟩ ∈ failures_{⊥} (P) | σ ≠ ϵ ∨ ¬stable(P)} ∪
{⟨σ,X⟩ ∈ failures_{⊥} (Q) | σ ≠ ϵ ∨ ¬stable(Q)} ∪
{⟨ϵ,X⟩ | ⟨ϵ,X⟩ ∈ failures_{⊥} (P) ∩ failures_{⊥} (Q)},
inf_{⊥} (P + Q) = inf_{⊥} (P) ∪ inf_{⊥} (Q)
divergences_{⊥} (P + Q) = divergences_{⊥} (P) ∪ divergences_{⊥} (Q) .

That it is a congruence for action prefixing, |, \L and [f] follows since

stable(α.P) iff α ≠ τ
stable(P|Q) iff stable(P) ∧ stable(Q) ∧ ¬∃ a ∈ A. (⟨a,∅⟩ ∈ failures_{⊥} (P) ∧ ⟨ā,∅⟩ ∈ failures_{⊥} (P))
stable(P\L) iff stable(P)
stable(P[f]) iff stable(P).

By definition, ⊑_{+reward}^{τ} is contained in ⊑_{+reward} . To see that it is the coarsest precongruence contained in ⊑_{+reward} , suppose P ⋢_{+reward}^{τ} Q. It suffices to build a context C[ ] from CCS operators such that C[P] ⋢_{+reward} C[Q]. The case P ⋢_{+reward} Q is immediate—take the trivial context with C[P] := P. So assume P ⊑_{+reward} Q. Then stable(P) and ¬stable(Q). Hence ϵ ∉ divergences_{⊥} (P) ⊇ divergences_{⊥} (Q). Choose a ∉ ptraces(Q)—in case no such a exists, one first applies an injective relabelling to P and Q such that a ∉ range(f). Now ⟨ϵ,{a}⟩ ∈ failures(Q) ⊆ failures_{⊥} (Q) ⊆ failures_{⊥} (P). However, whereas ⟨ϵ,{a}⟩ ∈ failures_{⊥} (Q + a) one has ⟨ϵ,{a}⟩ ∉ failures_{⊥} (P + a). It follows that P + a ⋢_{+reward} Q + a.

The arguments for X ∈ {reward, fp-reward} are very similar. □

12 Axiomatisations

The following axioms are easily seen to be sound for ⊑_{reward}^{τ}. Here an equality P ≡ Q can be seen as a shorthand for the two axioms P ⊑ Q and Q ⊑ P. Action prefixing and Δ bind stronger than +.

{  (R1)  τ.X + Y ≡ τ.X + τ.(X + Y)
(R2) α.X + τ.(α.Y + Z) ≡ τ(α.X + α.Y + Z)
(R3) α.(τ.X + τ.Y) ≡ α.X + α.Y }
(RP1)  τ.X + Y ⊑ τ.(X + Y)
(RP2)  τ.X + Y ⊑ X
(R4)  τ.ΔX + Y ≡ Δ(X + Y)

For recursion-free processes, and dropping the infinite choice operator in favour of + and 0, ⊑_{must}^{τ} coincides with ⊑_{reward}^{τ} and ⊑_{fp-reward}^{τ}. Together with the standard axioms for strong bisimilarity [24], the three axioms (R1)–(R3) constitute a sound and complete axiomatisation of ≡_{must}^{τ} [5, Theorem 4.2], and thus for ≡_{reward}^{τ}. Likewise, the three axioms (RP1),(RP2) and (R3) constitute a sound and complete axiomatisation of ⊑_{must}^{τ}[5, Theorem 4.1], and thus for ⊑_{reward}^{τ}; the axioms (R1) and (R2) are derivable from them. The first sound and complete axiomatisation of ⊑_{must}^{τ}appears in [6]; their axioms are derivable from the ones above (and vise versa).

A sound and complete axiomatisation of ≡_{may} (and hence of ≡_{−reward} ) is obtained by adding the axioms τ.X ≡ X and α(X + Y) ≡ α.X + α.Y to the standard axioms for strong bisimilarity [5, Theorem 4.5]. The axioms (R1)–(R3) are derivable from them. Adding the axiom X + Y ⊑ X yields a sound and complete axiomatisation of ⊑_{may}^{−1} (and hence of ⊑_{−reward} ) [5, Theorem 4.6]. The axioms (RP1) and (RP2) are then also derivable. The first sound and complete axiomatisation of ⊑_{may}appears in [6]; their axioms are derivable from the ones above (and vise versa).

To illustrate the difference between ≡_{must}^{τ}and ≡_{reward}^{τ}, without having to deal with recursion, I consider recursion-free CCS with finite choice (as done above), but upgraded with the delay operator Δ introduced in [3] and in Section 9. Clearly all preorders of this paper are precongruences for Δ. With (R4), sound for ≡_{reward}^{τ}, one can derive τ.ΔX ≡ ΔX and ΔX + Y ≡ Δ(X + Y). Writing Ω for Δ0, the latter implies ΔY ≡ Ω + Y so one can equally well take Ω as Δ as primitive. It also follows that ΔΔX ≡ ΔX.

The above sound and complete axiomatisations of ≡_{may} and ⊑_{may}^{−1} (and hence of ≡_{−reward} and ⊑_{−reward} ) are extended with Δ by adding the trivial axiom ΔX = X; (R4) is then derivable. This illustrates that these preorders abstract from divergence. The axiom

(R5) ΔX ≡ ΔY

is sound for ≡_{must}^{τ}. It expresses that must testing does not record any information past a divergence. Axioms (RP2), (R4) and (R5) imply Ω ⊑ X, an axiom featured in [6]. Neither ΔX = X nor (R5) is sound for ≡_{reward}^{τ}.

13 Failure of congruence property for recursion

Each preorder ⊑ on CCS processes (= closed CCS expressions) can be extended to one on all CCS expressions by defining E ⊑ F iff all closed substitution instances of this inequality hold.

Definition 8 A preorder ⊑ on 𝔼_{CCS} is a (full) precongruence for recursion if S_{Y} ⊑ T_{Y} for each Y ∈ dom(S) = dom(T) implies fix⦇X:S⦈ ⊆ fix⦇X:T ⦈.

The following counterexample shows that the must-testing preorder ⊑_{must}^{τ}fails to be a precongruence for recursion, implying that the must-testing equivalence ≡_{must}^{τ}fails to be a congruence for recursion.

Example 6 Let P ∈ 𝕋_{CCS} be such that ϵ ∉ divergences(P)—for instance P = 0. Then by (R1) one has τ.P + X ≡_{must}^{τ}τ.P + τ.(X + P). Yet fix⦇X:X =^{def} τ.P + X⦈ ⋢_{must}^{τ}fix⦇X:X =^{def} τ.P + τ.(X + P)⦈, because only the latter process has a divergence ϵ.

The same example shows that also ⊑_{reward}^{τ}, ⊑_{fp-reward}^{τ}, ⊑_{reward}, ⊑_{fp-reward} and ⊑_{must}fail to be precongruences for recursion. However, I conjecture that all these preorders are lean precongruences for recursion as defined in [14].

14 Unguarded recursion

The must-testing preorder ⊑_{must}on CCS presented in this paper is not quite the same as the original one ⊑_{must}^{org}from [6]. The following example shows the difference.

Example 7  0  ≡_{must} ; ⋢_{must}^{org}  fix⦇X:X =^{def} X⦈  \begin{matrix}⋢_{must} \\ ≡_{must}^{org} \end{matrix}  fix⦇X:X =^{def} τ.X⦈.

The ≡_{must}-statement follows since neither process has a single outgoing transition; the processes are even strongly bisimilar [24]. The ⋢_{must}-statement follows since ϵ ∈ divergences(fix⦇X:X =^{def} τ.X⦈), yet ϵ ∉ divergences(fix⦇X:X =^{def} X⦈) . A test showing the difference is τ.ω.

The reason that in the original must-testing approach fix⦇X:X =^{def} X⦈ sides with fix⦇X:X =^{def} τ.X⦈ rather than with 0, is that [6] treats a process featuring unguarded recursion (cf. [24]), such as fix⦇X:X =^{def} X⦈, as if it diverges, regardless whether it can do any internal actions τ. This leads to a must-testing equivalence that is incomparable with strong bisimilarity.

In my view, the decision whether fix⦇X:X =^{def} X⦈diverges or not is part of the definition of the process algebra CCS, and entirely orthogonal to the development of testing equivalences. Below I define a process algebra CCS_{⊥} that resembles CCS in all aspects, expect that any process with unguarded recursion is declared to diverge. I see the work of [6] not so much as defining a must-testing equivalence on CCS that is incomparable with strong bisimilarity, but rather as defining a must-testing equivalence on CCS_{⊥}, a languages that is almost, but not quite, the same as CCS.^{2} This is a matter of opinion, as there is no technical difference between these approaches.

I now proceed to define CCS_{⊥}, and apply the reward testing preorders of this paper to that language.

Definition 9 Let ↓ be the least predicate on ℙ_{CCS} which satisfies • α.P ↓ for any α ∈ Act,

• if P_{i}↓ for all i ∈ I then ∑_{i∈I} P_{i}↓,

• if P ↓ and Q↓ then P|Q↓, P\L↓ and P[f]↓,

• if fix⦇S_{X}:S⦈↓ then fix⦇X:S⦈↓.

Let P ↑ if not P ↓. If P ↑ then P features strongly unguarded recursion.^{3}

Note that 0↓, fix⦇X:X =^{def} X⦈↑ and fix⦇X:X =^{def} τ.X⦈↓, the latter because in Definition 9 τ is allowed as a guard. The definitions of this paper are adapted to CCS_{⊥} by redefining P diverges, notation P⇑, if either there is a P′with P =⇒ P′↑ or there are P_{i} ∈ ℙ for all i > 0 such that P −→^{τ} P_{1} −→^{τ} P_{2} −→^{τ} ··· . In Definition 2, and similarly for Definition 1, clause (i) is replaced by (i′) “if T_{n} is the final element in π, then either T_{n}↑ or T_{n} −→^{τ,r} Tfor no r and T ”. Now all results for CCS from Sections 3–12 remain valid for CCS_{⊥} as well. The only change in the proofs of Theorems 1–3, direction “⇐”, is that finite paths ending in ↓ are treated like infinite paths.

My definition of ⊑_{must}on CCS_{⊥} differs on two points from the definition of ⊑_{must}on CCS_{⊥} from [6]. But both differences are inessential, and the resulting notion of ⊑_{must}is the same. The first difference is that in [6] the notion of computation is exactly as in Definition 1, rather than the amended form above. However, in [6] a computation π = T_{0},T_{1},T_{2},...∈ Comp(T |P) counts as successful only if (a) it contains a state T with T −→^{ω} T′for some T′, and (b) if T_{k}↑ then T_{k′} −→^{ω} T′for some T′and some k′≤ k. It is straightforward to check that Apply(T|P) remains the same upon dropping (b) and changing (i) into (i′). The other difference is that in [6] τ does not count as a guard—their version of Definition 9 requires α ∈ A. So in [6] one has fix⦇X:X =^{def} τ.X⦈↑ . The notion of ↓ from [6] is therefore closer to unguarded recursion rather than strongly unguarded recursion. However, in the treatment of [6] one would have fix⦇X:X =^{def} a.X|ā⦈↓, showing that the resulting notion of guardedness is not very robust. Since the essential difference between CCS and CCS_{⊥} is that in CCS_{⊥} a strongly unguarded recursion is treated as a divergence, it does not matter whether ↓ also includes all or some not-strongly unguarded recursions, such as fix⦇X:X =^{def} τ.X⦈ . For any such not-strongly unguarded recursion is already divergent, and hence it does not make difference whether it is declared syntactically divergent as well.

An alternative to moving from CCS to CCS_{⊥} is to restrict either language to processes P satisfying P ↓. This restriction rules out the process fix⦇X:X =^{def} X⦈, but includes fix⦇X:X =^{def} τ.X⦈ . On this restricted set of processes their is no difference between CCS and CCS_{⊥}.

2All processes of Example 7 are weakly bisimilar [24]. In my view this does not mean that weak bisimulation semantics uses a variant of CCS in which none of these processes diverges. Instead it tells that weak bisimilarity abstracts from divergence.

3Un(strongly unguarded) recursion should not be called “strongly guarded” recursion; it is weaker than guarded recursion.

Another approach to making unguarded recursions divergent is to change the rule (Rec) from Table 1 into fix⦇X:S⦈ −→^{τ} fix⦇S_{X}:S⦈; this is done in the setting of CSP [26]. This would not have the same result, however, as here and in [6] one has a + fix⦇X:X =^{def} b⦈ ≡_{must}a + b .

The great advantage of moving from CCS to CCS_{⊥} is that Counterexample 6, against testing preorders being congruences for recursion, disappears.

Question 1 Are ⊑_{reward}^{τ}, ⊑_{fp-reward}^{τ} and ⊑_{must}^{τ}precongruences for recursion on CCS_{⊥}?

In [6] it is shown that, in the absence of infinite choice, ⊑_{must}^{τ}is a precongruences for recursion. Central in the proof is that on CCS_{⊥} with finite choice, the clause on infinite traces (inf_{⊥} (P) ⊇ inf_{⊥} (Q)) may be dropped from Theorem 3, since the infinite traces inf_{⊥} (P) of a CCS_{⊥} process P with finite choice are completely determined by divergences_{⊥} (P) and failures_{⊥} (P). This proof does not generalise to ⊑_{reward}^{τ} or ⊑_{fp-reward}^{τ}, since here, on CCS_{⊥} with finite choice, the infinite traces are not redundant. The proof also does not generalise to ⊑_{must}^{τ}on CCS with infinite choice.

In [28] it is shown that ⊑_{FDI}^{⊥} (cf. Theorem 3), which coincides with ⊑_{must}, is a congruence for recursion on the language CSP. I expect that similar reasoning can show that ⊑_{reward}^{τ} is a congruence for recursion on CCS_{⊥}. In [29] it is shown that ⊑_{FDI}^{d} (cf. Theorem 2), which coincides with ⊑_{fp-reward}, is a congruence for recursion on CSP. I expect that similar reasoning can show that ⊑_{fp-reward}^{τ} is a congruence for recursion on CCS_{⊥}. Roscoe [29] also presents an example, independently discovered by Levy [23], showing that ≡_{NDFD} (cf. Theorem 1), which coincides with ⊑_{reward}, fails to be a congruence for recursion:^{4} Let FA be a process that has all conceivable failures, divergences and infinite traces, except for the infinite trace a^{∞}. Then FA + τ.X ≡_{NDFD} FA + a.X, for both sides have all conceivable failures, divergences and infinite traces, with the possible exception of a^{∞}, and both side have the infinite trace a^{∞} iff X has it. However,

fix⦇X:FA + τ.X⦈ ≢_{NDFD} fix⦇X:FA + a.X⦈

since only the latter process has the infinite trace a^{∞}.

It could be argued that this example shows that the definition of being a congruence for recursion ought to be sharpened, for instance by requiring that E ⊑ F holds only if all closed substitutions of E ⊑ F employing an extended alphabet of actions hold. This would invalidate FA+τ.X ≡_{NDFD} FA+a.X, namely by substituting b for X, with b a fresh action, not alluded to in FA. With such a sharpening, the question whether ⊑_{reward}^{τ}is a congruence for recursion on CCS_{⊥} is open.

15 Related work

The concept of reward testing stems from [18], in the setting of nondeterministic probabilistic processes. In the terminology of Section 7, they employ single reward nonnegative reward testing. In [10] it was shown, again in a probabilistic setting, that nonnegative reward testing is no more powerful then classical testing. This result is a probabilistic analogue of Theorem 7. Negative rewards were first proposed in [11], a predecessor of the present paper. In [8], reward testing with also negative rewards, called realreward testing, was applied to nondeterministic probabilistic processes. Although technically no rewards can be gathered after a first reward has been encountered, thanks to probabilistic branching rewards can be distributed over multiple actions in a computation. This makes the approach a probabilistic generalisation of the reward testing proposed here. The main result of [8] is that for finitary (= finite-state and finitely many transitions) nondeterministic probabilistic processes without divergence, real-reward testing coincides with nonnegative reward testing. This is a generalisation (to probabilistic processes) of a specialisation (to finitary processes) of Proposition 1. An explicit characterisation (as in Theorem 1) of real-reward testing for processes with divergence was not attempted in [8].

4The example was formulated for another equivalence, but actually applies to a range of equivalences, including ≡_{NDFD}.

The nondivergent failures divergences equivalence, ≡_{NDFD}, defined in the proof of Theorem 1, stems from [19]. There it was shown to be the coarsest congruence (for a collection of operators equivalent to the ones used in Section 10) that preserves those linear-time properties (cf. Definition 7) that can be expressed in linear-time temporal logic without the nexttime operator. If follows directly from their proof that it is also the coarsest congruence that preserves all linear-time properties as defined in Definition 7; so ≡_{NDFD} coincides with ≡_{lt. properties}, as remarked at the end of Section 10. It is this result that inspired Theorem 1 in the current paper.

The paper [22] argues that ≡_{NDFD} can be seen as a testing equivalence, but does not offer a testing scenario in quite the same style as [6] or the current paper.

The semantic equivalence ≡_{FDI}^{d}, whose associated preorder occurs in the proof of Theorem 2, stems from [27]. There it was shown to be the coarsest congruence (for the same operators) that preserves deadlocks(P) ∪ divergences(P), the combined deadlock and divergence traces of a process (cf. Definition 3). It is this result that directly led (via [12, Theorem 9]) to Theorem 2 in the current paper.

In [6] the action ω is used merely to mark certain states as success states, namely the states were an ω-transition is enabled; a computation is successful iff it passes through such a success state. In [30], on the other hand, it is the actual execution of ω that constitutes success. In [10, 7], this is called actionbased testing; [7, Proposition 5.1 and Example 5.3] shows that action-based must testing is strictly less discriminating than state-based must-besting:

τ.a.Ω ≡_{must}^{action-based} τ.a.Ω + τ.0,  whereas  τ.a.Ω ⋢_{must}τ.a.Ω + τ.0.

The preorders in the current paper are generalisations of state-based testing; an action-based form of reward testing could be obtained by only allowing τ-actions to carry non-0 rewards. The same counterexample as above would show the difference between state- and action-based reward testing.

The reward testing contributed here constitutes a strengthening of the testing machinery of De Nicola & Hennessy. As such it differs from testing-based approaches that lead to incomparable preorders, such as the efficiency testing of [31], or the fair testing independently proposed in [4] and [25].

In [13] I advocate an overhaul of concurrency theory to ensure liveness properties when making the reasonable assumption of justness. The current work is prior to any such overhaul. It is consistent with the principles of [13] when pretending that the parallel composition | of CCS is in fact not a parallel composition of independent processes, but an interleaving operator, scheduling two parallel treads by means of arbitrary interleaving.

16 Conclusion

In this paper I contributed a concept of reward testing, strengthening the may and must testing of De Nicola & Hennessy. Inspired by [19, 27], I provided an explicit characterisation of the reward-testing preorder, as well as of a slight weakening, called finite-penalty reward testing. Must testing can be recovered by only considering positive rewards, and may testing by only considering negative rewards. While the must-testing preorder preserves liveness properties, and the inverse of the may-testing preorder (which can also be seen as a must-testing preorder dealing with catastrophes rather than successes) preserves safety properties, the (finite-penalty) reward testing preorder, which is finer than both, additionally preserves conditional liveness properties. I illustrated the difference between may testing, must testing and (finite-penalty) reward testing in terms of their equational axiomatisations. When applied to CCS as intended by Milner, must-testing equivalence fails to be a congruence for recursion, and the same problem exists for reward testing. The counterexample is eliminated by applying it to a small variant of Rob van Glabbeek 19

CCS that, following [6], treats a process with unguarded recursion as if it is diverging, even if it cannot make any internal moves. In this setting, by analogy with Roscoe’s work on CSP [28, 29], I expect musttesting and finite-penalty reward testing to be congruences for recursion; for reward testing this question remains open.

References

[1] S. Abramsky & A. Jung (1994): Domain Theory. In: Handbook of Logic and Computer Science, 3, Clarendon Press, pp. 1–168.

[2] B. Alpern & F.B. Schneider (1985): Defining liveness. Information Processing Letters 21(4), pp. 181–185,

doi:10.1016/0020-0190(85)90056-0.

[3] J.A. Bergstra, J.W. Klop & E.-R. Olderog (1987): Failures without chaos: a new process semantics for fair abstraction. In M. Wirsing, editor: Formal Description of Programming Concepts – III, Proceedings of the 3^{th}IFIP WG 2.2 working conference, Ebberup 1986, North-Holland, Amsterdam, pp. 77–103.

[4] E. Brinksma, A. Rensink & W. Vogler (1995): Fair Testing. In I. Lee & S. Smolka, editors: Proceedings 6th International Conference on Concurrency Theory, (CONCUR’95), Philadelphia, PA, USA, August 1995, LNCS 962, Springer, pp. 313–327, doi:10.1007/3-540-60218-6_23.

[5] T. Chen, W.J. Fokkink & R.J. van Glabbeek (2015): On the Axiomatizability of Impossible Futures. Logical Methods in Computer Science 11(3):17, doi:10.2168/LMCS-11(3:17)2015.

[6] R. De Nicola & M. Hennessy (1984): Testing equivalences for processes. Theoretical Computer Science 34,

pp. 83–133, doi:10.1016/0304-3975(84)90113-0.

[7] 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, doi:10.2168/LMCS-4(4:

4)2008.

[8] Y. Deng, R.J. van Glabbeek, M. Hennessy & C.C. Morgan (2014): Real-Reward Testing for Probabilistic Processes. Theoretical Computer Science 538, pp. 16–36, doi:10.1016/j.tcs.2013.07.016.

[9] Y. Deng, R.J. van Glabbeek, M. Hennessy, C.C. Morgan & C. Zhang (2007): Remarks on Testing Probabilistic Processes. In L. Cardelli, M. Fiore & G. Winskel, editors: Computation, Meaning, and Logic: Articles dedicated to Gordon Plotkin, Electronic Notes in Theoretical Computer Science 172, Elsevier, pp. 359–397,

doi:10.1016/j.entcs.2007.02.013.

[10] Y. Deng, R.J. van Glabbeek, C.C. Morgan & C. Zhang (2007): Scalar Outcomes Suffice for Finitary Probabilistic Testing. In R. De Nicola, editor: Proceedings 16th European Symposium on Programming, ESOP 2007, Braga, Portugal, LNCS 4421, Springer, pp. 363–378, doi:10.1007/978-3-540-71316-6_25.

[11] R.J. van Glabbeek (2009): The Linear Time Branching Time Spectrum after 20 years, or Full abstraction for safety and liveness properties. Copies of slides. Invited talk for IFIP WG 1.8 at CONCUR 2009 in Bologna.

Available at http://theory.stanford.edu/~rvg/abstracts.html#20years.

[12] R.J. van Glabbeek (2010): The Coarsest Precongruences Respecting Safety and Liveness Properties. In C.S. Calude & V. Sassone, editors: Proceedings 6th IFIP TC 1/WG 2.2 International Conference on Theoretical Computer Science (TCS 2010); held as part of the World Computer Congress 2010, Brisbane, Australia, IFIP 323, Springer, pp. 32–52, doi:10.1007/978-3-642-15240-5_3.

[13] R.J. van Glabbeek (2016): Ensuring Liveness Properties of Distributed Systems (A Research Agenda). Posi-

tion paper. Available at https://arxiv.org/abs/1711.04240.

[14] R.J. van Glabbeek (2017): Lean and Full Congruence Formats for Recursion. In: Proceedings 32^{nd} Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 2017, IEEE Computer Society Press, doi:10.1109/LICS.2017.8005142.

[15] R.J. van Glabbeek & P. Höfner (2015): Progress, Fairness and Justness in Process Algebra. Technical Report 8501, NICTA, Sydney, Australia. Available at http://arxiv.org/abs/1501.03268.

20 Reward Testing Equivalences for Processes

[16] M. Hennessy (1982): Powerdomains and nondeterministic recursive definitions. In: Proceedings 5th Intern. Symposium on Programming, LNCS 137, Springer, pp. 178–193, doi:10.1007/3-540-11494-7_13.

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

[18] B. Jonsson, C. Ho-Stuart & W. Yi (1994): Testing and Refinement for Nondeterministic and Probabilistic Processes. In: Proceedings of the 3rd International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS 863, Springer, pp. 418–430, doi:10.1007/3-540-58468-4_176.

[19] R. Kaivola & A. Valmari (1992): The Weakest Compositional Semantic Equivalence Preserving Nexttimeless Linear Temporal Logic. In R. Cleaveland, editor: CONCUR’92, LNCS 630, Springer, pp. 207–221,

doi:10.1007/BFb0084793.

[20] L. Lamport (1977): Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering 3(2), pp. 125–143, doi:10.1109/TSE.1977.229904.

[21] L. Lamport (1998): Proving Possibility Properties. Theoretical Computer Science 206(1-2), pp. 341–352,

doi:10.1016/S0304-3975(98)00129-7. See especially http://research.microsoft.com/en-us/
um/people/lamport/pubs/pubs.html#lamport-possibility.

[22] G. Leduc (1994): Failure-based congruences, unfair divergences and new testing theory. In S.T. Vuong & S.T. Chanson, editors: Proceedings Fourteenth IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification, Vancouver, BC, Canada, 1994, IFIP Conference Proceedings 1, Chapman & Hall, pp. 252–267.

[23] P.B. Levy (2008): Infinite trace equivalence. Annals of Pure and Applied Logic 151(2-3), pp. 170–198,

doi:10.1016/j.apal.2007.10.007.

[24] R. Milner (1990): Operational and algebraic semantics of concurrent processes. In J. van Leeuwen, editor: Handbook of Theoretical Computer Science, chapter 19, Elsevier Science Publishers B.V. (North-Holland), pp. 1201–1242. Alternatively see Communication and Concurrency, Prentice-Hall, Englewood Cliffs, 1989.

[25] V. Natarajan & R. Cleaveland (1995): Divergence and Fair Testing. In Z. Fülöp & F. Gécseg, editors: Proceedings 22nd International Colloquium on Automata, Languages and Programming (ICALP’95), Szeged, Hungary, July 1995, LNCS 944, Springer, pp. 648–659, doi:10.1007/3-540-60084-1_112.

[26] E.-R. Olderog & C.A.R. Hoare (1986): Specification-oriented semantics for communicating processes. Acta Informatica 23, pp. 9–66, doi:10.1007/BF00268075.

[27] A. Puhakka (2001): Weakest Congruence Results Concerning “Any-Lock”. In N. Kobayashi & B. Pierce, editors: Proceedings 4th International Symposium on Theoretical Aspects of Computer Software, TACS 2001, Sendai, Japan, 2001, LNCS 2215, Springer, pp. 400–419, doi:10.1007/3-540-45500-0_20.

[28] A.W. Roscoe (1997): The Theory and Practice of Concurrency. Prentice-Hall. Available at http://www.

comlab.ox.ac.uk/bill.roscoe/publications/68b.pdf.

[29] A.W. Roscoe (2005): Seeing Beyond Divergence. In A.E. Abdallah, C.B. Jones & J.W. Sanders, editors: Communicating Sequential Processes: The First 25 Years, Symposium on the Occasion of 25 Years of CSP, London, UK, 2004, Revised Invited Papers, LNCS 3525, Springer, pp. 15–35, doi:10.1007/11423348_2.

[30] R. Segala (1996): Testing Probabilistic Automata. In: Proceedings of the 7th International Conference on Concurrency Theory, LNCS 1119, Springer, pp. 299–314, doi:10.1007/3-540-61604-7_62.

[31] W. Vogler (2002): Efficiency of asynchronous systems, read arcs, and the MUTEX-problem. Theoretical Computer Science 275(1-2), pp. 589–631, doi:10.1016/S0304-3975(01)00300-0.