GDP Festschrift ENTCS, to appear

Remarks on Testing Probabilistic Processes

Yuxin Deng^{B,1} Rob van Glabbeek^{A,B} Matthew Hennessy^{C,A,2}
Carroll Morgan^{B,1} Chenyi Zhang^{A,B}

A National ICT Australia, Locked Bag 6016, Sydney, NSW 1466, Australia

B School of Computer Science and Engineering, The University of New South Wales, Sydney, Australia

C Department of Informatics, University of Sussex, Falmer, Brighton, BN1 9QN, UK

Abstract

We develop a general testing scenario for probabilistic processes, giving rise to two theories: probabilistic may testing and probabilistic must testing. These are applied to a simple probabilistic version of the process calculus CSP. We examine the algebraic theory of probabilistic testing, and show that many of the axioms of standard testing are no longer valid in our probabilistic setting; even for non-probabilistic CSP processes, the distinguishing power of probabilistic tests is much greater than that of standard tests. We develop a method for deriving inequations valid in probabilistic may testing based on a probabilistic extension of the notion of simulation. Using this, we obtain a complete axiomatisation for non-probabilistic processes subject to probabilistic may testing.

Keywords: Probabilistic processes, nondeterminism, CSP, transition systems, testing equivalences, simulation, complete axiomatisations, structural operational semantics

1 Introduction

Operational semantics has played a useful role in computer science since the very inception of the subject [Lan63,ER64,Luc71,BJ78]. But with the publication of [Plo81] (republished as [Plo04]) came the realisation that, properly structured, operational semantics provides an elegant compositional method for specifying the semantics of programming languages. Because of its mathematical foundations, structural operational semantics can also be used to reason about the behavioural properties of programs, to the extent it even brings into question the necessity of denotational semantics.

Nowhere is the power of operational semantics more evident than in the development of process calculi: the semantic theory underlying CCS [Mil89], bisimulation

1 We acknowledge the support of the Australian Research Council (ARC) Grant DP034557. 2 This research was carried out while on a Royal Society/Leverhulme Trust Senior Research Fellowship.

equivalence, is founded entirely on operational semantics. It provides powerful co-inductive proof methods for establishing process equivalences; it also supports compositional and algebraic reasoning techniques.

With CSP [Hoa85] the story is somewhat different: the failures model [BHR84] is denotational and was used to justify the algebraic laws so characteristic of the subsequent development of CSP as a specification language for processes. However, it later became apparent that, just as for CCS, this model and its algebraic theory could be fully justified using purely operational concepts based on notions of process testing [OH86,DH84]. So with CSP we have the best of all possible worlds:

• a denotational model,

• an operational model and

• an algebraic theory, all of which are in some sense equivalent.

The topic of this paper is probabilistic process calculi. The various semantic approaches for standard process calculi are essentially theories of nondeterministic processes, where the nondeterminism represents possible choices that can be resolved in a wholly unpredictable way. With probabilistic constructs the resolution becomes predictable up to a point, in that it is quantified; but the interaction between the quantified and unquantified forms of choice then requires close attention. The issue is mainly that the two forms of choice differ, not that one is quantified and the other is not: for example, a similar effect occurs when considering demonic and angelic choice together. Because they differ it is necessary to consider carefully the order in which they occur, and how they might or might not distribute over each other.

The first papers on probabilistic process calculi [GJS90,Chr90,LS92] proceed by replacing nondeterministic with probabilistic choice. The reconciliation of nondeterministic and probabilistic choice starts with [HJ90] and has received a lot of attention in the literature [JL91,WL92,JHW94,SL94,Low93,Low95,Seg95,MMSS96, PLS00,BS01,JW02,SV03], even in the sequential world [HSM97,MMS96], and, more recently, within general semantic domains [MM01,Mis00,MOW04,TKP05,VW06]; as such it could be argued that it is one of the central problems of the area. And CSP makes the issue more interesting still, by having two forms of choice already (both internal and external), so that probabilistic choice becomes the third.

The emphasis in this paper is on the development of an algebraic theory. Following [WL92] we adapt the original idea of testing [DH84] to probabilistic processes, arriving at two refinement relations between processes, the probabilistic may preorder and the probabilistic must preorder. For example P ⊑_{pmay} Q means that the probability that Q might pass a test is at least as good as the probability that P might pass it. We then apply this general framework of probabilistic testing to a simple finite probabilistic process algebra, pCSP, obtained by adding a probabilistic choice operator to a cut-down version of CSP. In order to do so we first need to interpret pCSP as a probabilistic labelled transition system [JWL01,HJ90,Seg95], a generalisation of the well known concept of labelled transition system, which describes the interactions which processes may have with their users.

With these generalisations it turns out that very few of the attractive algebraic laws underlying the algebraic theory of CSP, and indeed its denotational model, remain valid in the presence of probabilistic choice; this is demonstrated by a series of counterexamples, consisting of tests which distinguish process expressions previously identified. The main result of the paper is the development of a method for demonstrating positive algebraic identities. We develop a notion of simulation for probabilistic processes, writing P ⊑_{S} Q to mean that process Q can simulate the behaviour or P. We then go on to show

• the simulation relation ⊑_{S} is preserved by all the operators in pCSP

• the simulation relation is included in the probabilistic may preorder: P ⊑_{S} Q implies P ⊑_{pmay} Q.

This enables us to develop an algebraic theory for probabilistic may testing, which we briefly outline. The concept of simulation can also be adapted, by introducing a notion of failure, to obtain similar results for the probabilistic must preorder; but in order to keep the paper concise, the details are omitted. We do however show that, as expected, the theory based on must testing is more discriminating than that based on may testing; specifically P ⊑_{pmust} Q implies Q ⊑_{pmay} P.

In the final section we re-examine the behaviour of standard (non-probabilistic) CSP, using probabilistic tests. We show that these are in general more discriminating than non-probabilistic tests, and we give a complete equational characterisation for the resulting may theory.

Although this paper develops an algebraic theory of probabilistic testing in terms of pCSP, we could have obtained similar results using probabilistic versions of CCS or ACP, because processes defined in these calculi can be interpreted likewise.

2 Testing processes

It is natural to view the semantics of processes as being determined by their ability to pass tests [DH84,Hen88,BHR84,WL92,Seg96]; 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}.

Let us first set up a general testing scenario, within which this idea can be formulated. It assumes

• a set of processes Proc

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

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

• a function Apply : T × Proc → 𝒫fin^{+}(O), representing the possible results of applying a specific test to a specific process.

Here 𝒫fin^{+}(O) denotes the collection of finite non-empty subsets of O; 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. A more general theory would allow Apply(T, P) to be an arbitrary non-empty subset of O, but for the class of finite processes we consider in this paper, a finite set of outcomes turns out to be sufficient.

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 we can assume that O 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 we need to compare subsets of O. There are two standard approaches to make this comparison, based on viewing these sets as elements of either the Hoare or Smyth powerdomain [Hen82,AJ94] of O. For O_{1}, O_{2} ∈ 𝒫fin^{+}(O) we 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 we obtain two different semantic preorders for processes:

(i) For P, Q ∈ Proc 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.

We 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 ⊆ O be an upwards-closed subset of O, i.e. satisfying o′ ≥ o ∈ Pass ⇒ o′ ∈ Pass, thought of as the set of outcomes that can be regarded as passing a test. Then we say 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 ∈ T ∀Pass ∈ 𝒫^{↑}(O) (P may Pass T ⇒ Q may Pass T) P ⊑_{must} Q iff ∀T ∈ T ∀Pass ∈ 𝒫^{↑}(O) (P must Pass T ⇒ Q must Pass T)

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

The original theory of testing [DH84,Hen88] is obtained by using as the set of outcomes O the two-point lattice

⊥ ⊤

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

However, for probabilistic processes we consider an application of a test to a process to succeed with a given probability. Thus we take as the set of outcomes the unit interval [0, 1], with the standard mathematical ordering; if 0 ≤ p < q ≤ 1 then succeeding with probability q is considered better than succeeding with probability p. This yields two preorders for probabilistic processes, which for convenience we rename ⊑_{pmay} and ⊑_{pmust}, with the associated equivalences ≃_{pmay} and ≃_{pmust} respectively. These preorders, and their associated equivalences, were first defined by Wang and Larsen [WL92]. The purpose of the current paper is to apply them to a simple probabilistic process algebra.

Before doing so let us first point out a useful simplification: the Hoare and Smyth preorders on finite subsets of [0, 1] (and more generally on closed subsets of [0, 1]) are determined by their maximum and minimum elements respectively.

Proposition 2.1 For O_{1}, O_{2} ∈ 𝒫fin^{+}(O_{prob}) we have

(i) O_{1} ⊑_{Ho} O_{2} if and only if max(O_{1}) ≤ max(O_{2}) (ii) O_{1} ⊑_{Sm} O_{2} if and only if min(O_{1}) ≤ min(O_{2}).

Proof. Straightforward calculations. □

As in the non-probabilistic case [DH84], we could also define a testing preorder combining the may- must-preorders; we will not study this combination here.

3 Finite probabilistic CSP

We first define the language and its operational semantics. Then we show how the general probabilistic testing theory just outlined can be applied to processes from this language.

3.1 The language

Let Act be a set of actions, ranged over by a, b, c, …, which processes can perform. Then the finite probabilistic CSP processes are given by the following syntax:

P ::= 0 | a.P | P ⊓ P | P □ P | P |_{A} P | P_{p}⊕ P

The intuitive meaning of the various constructs is straightforward:

(i) 0 represents the stopped process. (ii) a.P, where a is in Act, is a process which first performs the action a, and then

proceeds as P. (iii) P ⊓ Q is the internal choice between the processes P and Q; it will act either

like P or like Q, but a user is unable to influence which. (iv) P □ Q is the external choice between P and Q; again it will act either like P

or like Q but, in this case, according to the demands of a user.

(v) P |_{A} Q, where A is a subset of Act, represents processes P and Q running in parallel. They may synchronise by performing the same action from A simultaneously; such a synchronisation results in an internal action τ ∉ Act. In addition P and Q may independently do any action from (Act \ A) ∪ {τ}.

(vi) P _{p}⊕ Q, where p is an arbitrary probability, a real number strictly between 0 and 1, is the probabilistic choice between P and Q. With probability p it will act like P and with probability (1−p) it will act like Q.

We use pCSP to denote the set of terms defined by this grammar, and CSP denotes the subset of that which does not use the probabilistic choice. Of course the language CSP in all its glory [BHR84,Hoa85,OH86] has many more operators; we have simply chosen a representative selection, adding probabilistic choice to obtain an elementary probabilistic version of CSP. Our parallel operator is not a CSP primitive, but it can easily be expressed in terms of the CSP primitives—in particular P |_{A} Q = (P ∥_{A}Q)\A, where ∥_{A} and \A are the parallel composition and hiding operators of [OH86]. It can also be expressed in terms of the parallel composition, renaming and restriction operators of CCS. We have chosen this (non-associative) operator for its convenience in defining the application of tests to processes.

As usual we tend to omit occurrences of 0; the action prefixing operator a. binds stronger than any of the binary operators, and precedence between the binary operators will be indicated via brackets or spacing. We will also sometimes use n-ary versions of the binary operators, such as ⨁_{i∈I} p_{i}P_{i} with ∑_{i∈I} p_{i} = 1, and □_{i∈I} P_{i}.

3.2 Operational Semantics of pCSP

The above intuitive reading of the various operators can be formalised by an operational semantics which associates with each process term a graph-like structure representing the manner in which it may react to users’ requests. Let us briefly recall this procedure for (non-probabilistic) CSP.

Definition 3.1 A labelled transition system (LTS) is a triple ⟨S, Act_{τ} , →⟩, where

(i) S is a set of states (ii) Act_{τ} is a set of actions Act, augmented with a new action symbol τ to represent

synchronisations, and more generally internal unobservable activity (iii) → ⊆ S × Act_{τ} × S represents the effect of performing actions.

It is usual to use the more intuitive notation s ⟶^{α} s′ instead of (s, α, s′) ∈ →.

The operational semantics of CSP is obtained by endowing the set of terms with the structure of an LTS. Specifically

(i) the set of states S is taken to be all terms from the language CSP (ii) the action relations P ⟶^{α} Q are defined inductively on the syntax of terms.

A precise definition may be found in [OH86].

In order to interpret the full pCSP operationally we need to generalise the notion of LTS to take probabilities into account. First we need some notation for probability distributions. A (discrete) probability distribution over a set S is a mapping Δ : S → [0, 1] with ∑_{s∈S} Δ(s) = 1. The support of Δ is given by ⌈Δ⌉ := { s ∈ S | Δ(s) > 0 }. For our simple setting we only require distributions with finite support; let D(S), ranged over by Δ, Θ, Φ, denote the collection of all such distributions over S. We use \overline{s} to denote the point distribution, satisfying

\overline{s}(t) = \begin{cases}1 & if t = s, \\ 0 & otherwise \end{cases}

while if p_{i} ≥ 0 and Δ_{i} is a distribution for each i in some finite index set I, then ∑_{i∈I} p_{i} · Δ_{i} is given by

(∑_{i∈I} p_{i} · Δ_{i})(s) = ∑_{i∈I} p_{i} · Δ_{i}(s)

If ∑_{i∈I} p_{i} = 1 then this is easily seen to be a distribution in D(S), and we will sometimes write it as p_{1} · Δ_{1} + … + p_{n} · Δ_{n} when the index set I is {1, …, n}.

We can now present the probabilistic generalisation of an LTS: Definition 3.2 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 actions Act, augmented by a new action τ, as above (iii) → ⊆ S × Act_{τ} × D(S). As with LTSs, we usually write s ⟶^{α} Δ in place of (s, α, Δ) ∈ →. An LTS may be viewed as a degenerate pLTS, one in which only point distributions are used. We now mimic the operational interpretation of CSP as an LTS by associating with pCSP a particular pLTS ⟨S_{p}, Act_{τ} , →⟩. However there are two major differences:

(i) only a subset of terms in pCSP will be used as the set of states S_{p} in the pLTS (ii) terms in pCSP will be interpreted as distributions over S_{p}, rather than as

elements of S_{p}. First we define the subset S_{p} of states that we use: it is the least set satisfying

(i) 0 ∈ S_{p} (ii) a.P ∈ S_{p} (iii) P ⊓ Q ∈ S_{p} (iv) s_{1}, s_{2} ∈ S_{p} implies s_{1} □ s_{2} ∈ S_{p}

(v) s_{1}, s_{2} ∈ S_{p} implies s_{1} |_{A} s_{2} ∈ S_{p}. Thus, S_{p} is the set of pCSP expressions in which every occurrence of the probabilistic choice operator_{p}⊕ is weakly guarded, i.e. is within a subexpression of the form a.P or P ⊓ Q. The interpretation of terms in pCSP as distributions in D(S_{p}) is as follows:

(i) ⟦ 0 ⟧ = \overline{0} (ii) ⟦a.P ⟧ = \overline{a.P} (iii) ⟦P ⊓ Q⟧ = \overline{P ⊓ Q} (iv) ⟦P_{p}⊕ Q⟧ = p · ⟦P ⟧ + (1−p) · ⟦Q⟧

(v) ⟦P □ Q⟧ = ⟦P ⟧ □ ⟦Q⟧ (vi) ⟦P |_{A} Q⟧ = ⟦P ⟧ |_{A} ⟦Q⟧. In the last two cases we take advantage of the fact that both □ and |_{A} can be viewed

a.P ⟶^{a} ⟦P ⟧^{(action)}

P ⊓ Q ⟶^{τ} ⟦P ⟧^{(int.l)}  P ⊓ Q ⟶^{τ} ⟦Q⟧^{(int.r)}

\frac{s_{1} ⟶^{τ} Δ^{(ext.i.l)}}{s_{1} □ s_{2} ⟶^{τ} Δ □ \overline{s_{2}}}  \frac{s_{2} ⟶^{τ} Δ^{(ext.i.r)}}{s_{1} □ s_{2} ⟶^{τ} \overline{s_{1}} □ Δ}

\frac{s_{1} ⟶^{a} Δ^{(ext.l)}}{s_{1} □ s_{2} ⟶^{a} Δ}  \frac{s_{2} ⟶^{a} Δ^{(ext.r)}}{s_{1} □ s_{2} ⟶^{a} Δ}

\frac{s_{1} ⟶^{α} Δ^{(par.l)}}{s_{1} |_{A} s_{2} ⟶^{α} Δ |_{A} \overline{s_{2}}} ^{α ∉ A}  \frac{s_{2} ⟶^{α} Δ^{(par.r)}}{s_{1} |_{A} s_{2} ⟶^{α} \overline{s_{1}} |_{A} Δ} ^{α ∉ A}

\frac{s_{1} ⟶^{a} Δ_{1}, s_{2} ⟶^{a} Δ_{2}^{(par.i)}}{s_{1} |_{A} s_{2} ⟶^{τ} Δ_{1} |_{A} Δ_{2}} ^{a ∈ A}

Fig. 1. Operational semantics of pCSP. Here a ranges over Act and α over Act_{τ}.

as binary operators over S_{p}, and can therefore be lifted to D(S_{p}) in the standard manner. Namely we define

(Δ_{1} □ Δ_{2})(s) = \begin{cases}Δ_{1}(t_{1}) · Δ_{2}(t_{2}) & if s = t_{1} □ t_{2}, \\ 0 & otherwise \end{cases}

with Δ_{1} |_{A} Δ_{2} given similarly; note that as a result we have ⟦P ⟧ = \overline{P} for all P ∈ S_{p}. Finally the definition of the relations ⟶^{α} is given in Figure 1. These rules are very similar to the standard ones used to interpret CSP as an LTS [OH86], modified to take into account that the result of an action must be a distribution. For example (int.l) and (int.r) say that P ⊓ Q makes an internal unobservable choice to act either like P or like Q. Similarly the four rules (ext.l), (ext.r), (ext.i.l) and (ext.i.r) can be read as giving the standard interpretation to the external choice operator: the process P □ Q may perform any external action of its components P and Q, which resolves the choice; it may also perform any of their internal actions, but when these are performed the choice is not resolved.

3.3 The precedence of probabilistic choice

Our operational semantics entails that □ and |_{A} distribute over probabilistic choice:

\begin{aligned}⟦P □ (Q_{p}⊕ R)⟧ & = & ⟦(P □ Q)_{p}⊕ (P □ R)⟧ \\ ⟦P |_{A} (Q_{p}⊕ R)⟧ & = & ⟦(P |_{A} Q)_{p}⊕ (P |_{A} R)⟧ \end{aligned}

In Section 6.5, these identities will return as axioms of may testing. However, this is not so much a consequence of our testing methodology: it is hardwired in our interpretation ⟦ ⟧ of pCSP expressions as distributions. We could have obtained the same effect by introducing pCSP as a two-sorted language, given by the grammar

P ::= S | P_{p}⊕ P
S::= 0 | a.P | P ⊓ P | S □ S | S |_{A} S

and introducing expressions like P □ (Q _{p}⊕ R) and P |_{A} (Q _{p}⊕ R) as syntactic sugar for the grammatically correct expressions obtained by distributing □ and |_{A} over_{p}⊕. In that case, the S-expressions would constitute the set S_{p} of states in the pLTS of pCSP, and ⟦s⟧ = \overline{s} for any s ∈ S_{p}.

A consequence of our operational semantics is that in the process a.(b_{\frac{1}{2}} ⊕ c) |_{∅} d the action d can be scheduled either before a, or after the probabilistic choice between b and c—but it can not be scheduled after a and before this probabilistic choice. We justify this by thinking of P_{p}⊕ Q not as a process that starts with making a probabilistic choice, but rather as one that has just made such a choice, and with probability p is no more and no less than the process P. Thus a.(P_{p}⊕ Q) is a process that in doing the a-step makes a probabilistic choice between the alternative targets P and Q.

This design decision is in full agreement with previous work featuring nondeterminism, probabilistic choice and parallel composition [HJ90,WL92,Seg95]. Moreover, a probabilistic choice between processes P and Q that does not take precedence over actions scheduled in parallel can simply be written as τ.(P_{p}⊕ Q). Here τ.P is an abbreviation for P ⊓ P. Using the operational semantics of ⊓ in Figure 1, τ.P is a process whose sole initial transition is τ.P ⟶^{τ} P, hence τ.(P_{p}⊕ Q) is a process that starts with making a probabilistic choice, modelled as an internal action, and with probability p proceeds as P. Any activity scheduled in parallel with τ.(P_{p}⊕ Q) can now be scheduled before or after this internal action, hence before or after the making of the choice. In particular, a.τ.(b_{\frac{1}{2}} ⊕ c) |_{∅} d allows d to happen between a and the probabilistic choice.

3.4 Graphical representation of pCSP processes

We graphically depict the operational semantics of a pCSP expression P by drawing the part of the pLTS defined above that is reachable from ⟦P ⟧ as a finite acyclic directed graph. Given that in a pLTS transitions go from states to distributions, we need to introduce additional edges to connect distributions back to states, thereby obtaining a bipartite graph. States are represented by nodes of the form • and distributions by nodes of the form ∘. For any state s and distribution Δ with s ⟶^{α} Δ we draw an edge from s to Δ, labelled with α. Consequently, the edges leaving a •-node are all labelled with actions from Act_{τ}. For any distribution Δ and state s in ⌈Δ⌉, the support of Δ, we draw an edge from Δ to s, labelled with Δ(s). Consequently, the edges leaving a ∘-node are labelled with positive real numbers that sum up to 1. Because for our simple language the resulting directed bipartite graphs are acyclic, we leave out arrowheads on edges and we assume control to flow

1 ; \begin{matrix}d \\ 1 \end{matrix} abbrev. to d  \begin{aligned}& 1 \\ τ ; 1 ; \begin{matrix}b \\ 1 \end{matrix} & & τ ; 1 ; \begin{matrix}c \\ 1 \end{matrix} \end{aligned} abbrev. to _{\begin{matrix}τ \\ b \end{matrix} \begin{matrix}τ \\ c \end{matrix}}

i) d. 0  ii) b. 0 ⊓ c. 0

\begin{matrix}_{_{\begin{aligned}& τ \\ b & & d \end{aligned} d \begin{aligned}& τ \\ c & & d \end{aligned}}^{\frac{1}{2}}  _{\begin{aligned}& τ \\ b & & a \end{aligned} a \begin{aligned}& τ \\ c & & a \end{aligned}}^{\frac{1}{2}}} & _{a^{\frac{1}{3}} _{\begin{aligned}& τ \\ b & & d \end{aligned} d \begin{aligned}& τ \\ c & & d \end{aligned}}^{\frac{1}{3}}  _{\begin{aligned}& τ \\ b & & a \end{aligned} a \begin{aligned}& τ \\ c & & a \end{aligned}}^{\frac{1}{3}}} \\ iii) (b ⊓ c) □ (d_{\frac{1}{2}} ⊕ a) & iv) a_{\frac{1}{3}} ⊕ ((b ⊓ c) □ (d_{\frac{1}{2}} ⊕ a)) \end{matrix}

Fig. 2. Example pLTSs

from top to bottom.

A few examples are described in Figure 2. In i) we find ⟦d. 0 ⟧ as the point distribution \overline{d. 0}, represented by a tree with one edge from the root, labelled with the probability 1, to the state d. 0. In turn this state is represented as the subtree with one outgoing edge, labelled by the only possible action d to ⟦ 0 ⟧. Finally this is also a point distribution, represented as a subtree with one edge leading to a leaf, labelled by the probability 1.

These edges labelled by probability 1 occur so frequently that it makes sense to omit them, together with the associated nodes ∘ representing point distributions. With this convention ⟦d. 0 ⟧ turns out to be a simple tree with one edge labelled by the action d. The same convention simplifies considerably the representation of b ⊓ c in ii), resulting in an LTS detailing an internal choice between the two actions. Officially, the endnodes of this graph ought to be merged, as both of them represent the process 0. However, for reasons of clarity, in graphical representations we often unwind the underlying graph into a tree, thus representing the same state or distribution multiple times.

The interpretation of (b ⊓ c) □ (d_{\frac{1}{2}} ⊕ a) is more interesting. This requires clause (v) above in the definition of ⟦ ⟧, resulting in the distribution \overline{(b ⊓ c)} □ Δ, where Δ is the distribution resulting from the interpretation of (d _{\frac{1}{2}} ⊕ a), itself a two-point distribution mapping both the states d. 0 and a. 0 to the probability \frac{1}{2}. The result is again a two-point distribution, this time mapping the two states (b ⊓ c) □ d and (b ⊓ c) □ a to \frac{1}{2}. The end result in iii) is obtained by further interpreting these two states using the rules in Figure 1. Finally in iv) we show the graphical

(a.ω_{\frac{1}{4}} ⊕ (b □ c.ω)) |_{Act} (b □ c □ d)

a.ω |_{Act} (b □ c □ d) \frac{1}{4} (b □ c.ω) |_{Act} (b □ c □ d) \frac{3}{4} \begin{matrix}0 |_{Act} 0 \\ τ \end{matrix} _{ω |_{Act} 0 τ \begin{matrix}0 |_{Act} 0 \\ ω \end{matrix}}

Apply((a.ω_{\frac{1}{4}} ⊕ (b □ c.ω)), (b □ c □ d)) = \frac{1}{4} · \{0\} + \frac{3}{4} · \{0, 1\} = \{0, \frac{3}{4}\}

Fig. 3. Example of testing

representation which results when this term is combined probabilistically with the simple process a. 0.

To sum up, the operational semantics endows pCSP with the structure of a pLTS, and the function ⟦ ⟧ interprets process terms in pCSP as distributions in this pLTS, which can be represented by finite acyclic directed graphs (typically drawn as trees), with edges labelled either by probabilities or actions, so that edges labelled by actions and probabilities alternate (although in pictures we may suppress 1-labelled edges and point distributions).

3.5 Testing pCSP processes

Let us now turn to applying the testing theory from Section 2 to pCSP. As with the standard theory [DH84,Hen88], we use as tests any process from pCSP itself, which in addition can use a special symbol ω to report success. For example, a.ω_{\frac{1}{4}} ⊕ (b □ c.ω) is a probabilistic test, which 25% of the time requests an a action, and 75% requests that c can be performed. If it is used as must test the 75% that requests a c action additionally requires that b is not possible. As in [DH84,Hen88], it is not the execution of ω that constitutes success, but the arrival in a state where ω is possible. The introduction of the ω-action is simply a method of defining a success predicate on states without having to enrich the language of processes explicitly with such predicates.

Formally, let ω ∉ Act_{τ} and write Act^{ω} for Act ∪ {ω} and Act_{τ}^{ω} for Act ∪ {τ, ω}. In Figure 1 we now let a range over Act^{ω} and α over Act_{τ}^{ω}. Tests may have subterms ω.P, but other processes may not. To apply the test T to the process P we run them in parallel, tightly synchronised; that is, we run the combined process T |_{Act} P. Here P can only synchronise with T, and in turn the test T can only perform the success action ω, in addition to synchronising with the process being tested; of course both tester and testee can also perform internal actions. An example is provided in Figure 3, where the test a.ω _{\frac{1}{4}} ⊕ (b □ c.ω) is applied to the process b □ c □ d. We see that 25% of the time the test is unsuccessful, in that it does not reach a state where ω is possible, and 75% of the time it may be successful, depending on how the now internal choice between the actions b and c is resolved, but it is not the case that it must be successful.

⟦T |_{Act} P ⟧ is representable as a finite graph which encodes all possible interactions of the test T with the process P. It only contains the actions τ and ω. Each occurrence of τ represents a nondeterministic choice, either in T or P themselves, or as a nondeterministic response by P to a request from T, while the distributions represent the resolution of underlying probabilities in T and P. We use the structure ⟦T |_{Act} P ⟧ to define Apply(T, P), the non-empty finite subset of [0, 1] representing the set of probabilities that applying T to P will be a success.

First we define a function Results( ), which when applied to any state in S_{p} returns a finite subset of [0, 1]. The definition will require that it be also applied to distributions, and to do so we need to use choice functions for collecting elements from subsets of [0, 1]. Suppose R : S_{p} → 𝒫fin^{+}([0, 1]), and c : X → [0, 1], where X is a subset of S_{p}. Then we write c ∈_{X} R if c(s) ∈ R(s) for every s in X, and the results-collecting function can be defined as follows:

Results(s) = \begin{cases}\{1\} & if s ⟶^{ω}, \\ ⋃\{ Results(Δ) | s ⟶^{τ} Δ \} & if s −̸⟶^{ω}, s ⟶^{τ}, \\ \{0\} & otherwise \end{cases}

where

Results(Δ) = { ∑_{s∈⌈Δ⌉} Δ(s) · c(s) | c ∈_{⌈Δ⌉} Results }

However, instead of the explicit use of choice functions, we will tend to use the more convenient notation

Results(Δ) = Δ(s_{1}) · Results(s_{1}) + … + Δ(s_{n}) · Results(s_{n})

where ⌈Δ⌉ = {s_{1}, … s_{n}}. Note that Results( ) is indeed a well-defined function, because the pLTS ⟨S_{p}, Act_{τ} , →⟩ is finitely branching and well-founded.

For example consider the transition systems in Figure 4, where for reference we have labelled the nodes. Then Results(s_{1}) = {1, 0} while Results(s_{2}) = {1}, and therefore Results(Δ_{s}) = \frac{1}{2} · \{1, 0\} + \frac{1}{2} · \{1\} which, since there are only two possible choice functions c ∈_{⌈Δ_{s}⌉} Results, evaluates further to \{\frac{1}{2}, 1\}. Similarly Results(t_{1}) = Results(t_{2}) = {0, 1} and using the four choice functions c ∈_{⌈Δ_{t}⌉} Results, the calculation of Results(Δ_{t}) = \frac{1}{4} · \{0, 1\} + \frac{3}{4} · \{0, 1\} leads to \{0, \frac{1}{4}, \frac{3}{4}, 1\}.

Definition 3.3 For any P ∈ pCSP and T ∈ T let Apply(T, P) = Results(⟦T |_{Act}P ⟧).

With this definition we now have two testing preorders for pCSP, one based on may testing, P ⊑_{pmay} Q, and the other on must testing, P ⊑_{pmust} Q.

\begin{matrix}\begin{matrix}Δ_{s} \\ s_{1}_{\frac{1}{2}} ; _{\begin{matrix}τ \\ ω \end{matrix} τ} & s_{2}_{\frac{1}{2}} ; \begin{matrix}τ \\ ω \end{matrix} \end{matrix} & \begin{aligned}& Δ_{t} \\ t_{1}_{\frac{1}{4}} ; _{\begin{matrix}τ \\ ω \end{matrix} τ} & & t_{2}_{\frac{3}{4}} ; _{τ \begin{matrix}τ \\ ω \end{matrix}} \end{aligned} \\ Results(Δ_{s}) = \{\frac{1}{2}, 1\} & Results(Δ_{t}) = \{0, \frac{1}{4}, \frac{3}{4}, 1\} \end{matrix}

Fig. 4. Collecting results

4 Counterexamples

We will see in this section that many of the standard testing axioms are not valid in the presence of probabilistic choice. We also provide counterexamples for a few distributive laws involving probabilistic choice that may appear plausible at first sight. In all cases we establish a statement P ≄_{pmay} Q by exhibiting a test T such that max(Apply(T, P)) ≠ max(Apply(T, Q)) and a statement P ≄_{pmust} Q by exhibiting a test T such that min(Apply(T, P)) ≠ min(Apply(T, Q)). In case max(Apply(T, P)) > max(Apply(T, Q)) we find in particular that P ⋢_{pmay} Q, and in case min(Apply(T, P)) > min(Apply(T, Q)) we obtain P ⋢_{pmust} Q.

Example 4.1 The axiom a.(P_{p}⊕ Q) = a.P_{p}⊕ a.Q is unsound.

Consider the example in Figure 5. In R_{1} the probabilistic choice between b and c is taken after the action a, while in R_{2} the choice is made before the action has happened. These processes can be distinguished by the nondeterministic test T = a.b.ω ⊓ a.c.ω. First consider running this test on R_{1}. There is an immediate choice made by the test, effectively running either the test a.b.ω on R_{1} or the test a.c.ω; in fact the effect of running either test is exactly the same. Consider a.b.ω. When run on R_{1} the a action immediately happens, and there is a probabilistic choice between running b.ω on either b or c, giving as possible results {1} or {0}; combining these according to the definition of the function Results( ) we get \frac{1}{2} · \{0\} + \frac{1}{2} · \{1\} = \{\frac{1}{2}\}. Since running the test a.c.ω has the same effect, Apply(T, R_{1}) turns out to be the same set \{\frac{1}{2}\}.

Now consider running the test T on R_{2}. Because R_{2}, and hence also T |_{Act} R_{2}, starts with a probabilistic choice, due to the definition of the function Results( ), the test must first be applied to the probabilistic components, a.b and a.c, respectively, and the results subsequently combined probabilistically. When the test is run on a.b, immediately a nondeterministic choice is made in the test, to run either a.b.ω or a.c.ω. With the former we get the result {1}, with the latter {0}, so overall, for running T on a.b, we get the possible results {0, 1}. The same is true when we run it on a.c, and therefore Apply(T, R_{2}) = \frac{1}{2} · \{0, 1\} + \frac{1}{2} · \{0, 1\} = \{0, \frac{1}{2}, 1\}.

So we have R_{2} ⋢_{pmay} R_{1} and R_{1} ⋢_{pmust} R_{2}.

\begin{matrix}\begin{aligned}& a \\ b^{\frac{1}{2}} & & c^{\frac{1}{2}} \end{aligned} & _{\begin{matrix}a \\ b \end{matrix}^{\frac{1}{2}}  \begin{matrix}a \\ c \end{matrix}^{\frac{1}{2}}} & _{τ ; a ; \begin{matrix}b \\ ω \end{matrix} τ ; a ; \begin{matrix}c \\ ω \end{matrix}} \\ R_{1} = a.(b_{\frac{1}{2}} ⊕ c) & R_{2} = a.b_{\frac{1}{2}} ⊕ a.c & T = a.b.ω ⊓ a.c.ω \end{matrix}

\begin{matrix}_{τ ; \begin{aligned}& τ \\ \begin{matrix}τ \\ ω \end{matrix}^{\frac{1}{2}} & & \frac{1}{2} \end{aligned}  τ ; \begin{aligned}& τ \\ \frac{1}{2} & & \begin{matrix}τ \\ ω \end{matrix}^{\frac{1}{2}} \end{aligned}} & _{_{τ ; τ ; \begin{matrix}τ \\ ω \end{matrix} \begin{matrix}τ \\ τ \end{matrix}}^{\frac{1}{2}}  _{\begin{matrix}τ \\ τ \end{matrix} τ ; τ ; \begin{matrix}τ \\ ω \end{matrix}}^{\frac{1}{2}}} \\ T |_{Act} R_{1} & T |_{Act} R_{2} \\ Apply(T, R_{1}) = \{\frac{1}{2}\} & Apply(T, R_{2}) = \{0, \frac{1}{2}, 1\} \end{matrix}

Fig. 5. Counterexample: action prefix does not distribute over probabilistic choice

Example 4.2 The axiom a.(P ⊓ Q) = a.P ⊓ a.Q is unsound.

It is well known that this axiom is valid in the standard theory of testing, for nonprobabilistic processes. However, consider the instance R_{1} and R_{2} in Figure 6, and note that these processes do not contain any probabilistic choice. But they can be differentiated by the probabilistic test T = a.(b.ω_{\frac{1}{2}} ⊕ c.ω); the details are in Figure 6. There is only one possible outcome from applying T to R_{2}, the probability \frac{1}{2}, because the nondeterministic choice is made before the probabilistic choice. On the other hand when T is applied to R_{1} there are three possible outcomes, 0, \frac{1}{2} and 1, because effectively the probabilistic choice takes precedence over the nondeterministic choice. So we have R_{1} ⋢_{pmay} R_{2} and R_{2} ⋢_{pmust} R_{1}.

Example 4.3 The axiom a.(P □ Q) = a.P □ a.Q is unsound.

This axiom is valid in the standard may-testing semantics. However, consider the two processes R_{1} = a.(b □ c), R_{2} = a.b □ a.c and the probabilistic test T = a.(b.ω _{\frac{1}{2}} ⊕ c.ω). Now Apply(T, R_{1}) = \{1\} and Apply(T, R_{2}) = \{\frac{1}{2}\}. Therefore R_{1} ⋢_{pmay} R_{2} and R_{1} ⋢_{pmust} R_{2}.

\begin{matrix}\begin{aligned}& a \\ \begin{matrix}τ \\ b \end{matrix} & & \begin{matrix}τ \\ c \end{matrix} \end{aligned} & _{τ ; \begin{matrix}a \\ b \end{matrix} τ ; \begin{matrix}a \\ c \end{matrix}} & \begin{aligned}& a \\ \begin{matrix}b \\ ω \end{matrix}^{\frac{1}{2}} & & \begin{matrix}c \\ ω \end{matrix}^{\frac{1}{2}} \end{aligned} \\ R_{1} = a.(b ⊓ c) & R_{2} = a.b ⊓ a.c & T = a.(b.ω_{\frac{1}{2}} ⊕ c.ω) \end{matrix}

\begin{matrix}\begin{aligned}& τ \\ _{τ ; \begin{matrix}τ \\ ω \end{matrix} τ}^{\frac{1}{2}} & & _{τ τ ; \begin{matrix}τ \\ ω \end{matrix}}^{\frac{1}{2}} \end{aligned} & _{τ ; \begin{aligned}& τ \\ \begin{matrix}τ \\ ω \end{matrix}^{\frac{1}{2}} & & \frac{1}{2} \end{aligned}  τ ; \begin{aligned}& τ \\ \frac{1}{2} & & \begin{matrix}τ \\ ω \end{matrix}^{\frac{1}{2}} \end{aligned}} \\ T |_{Act} R_{1} & T |_{Act} R_{2} \\ Apply(T, R_{1}) = \{0, \frac{1}{2}, 1\} & Apply(T, R_{2}) = \{\frac{1}{2}\} \end{matrix}

Fig. 6. Counterexample: action prefix does not distribute over internal choice

Example 4.4 The axiom P = P □ P is unsound.

Let R_{1}, R_{2} denote (a _{\frac{1}{2}} ⊕ b) and (a _{\frac{1}{2}} ⊕ b) □ (a _{\frac{1}{2}} ⊕ b), respectively. It is easy to calculate that Apply(a.ω, R_{1}) = \{\frac{1}{2}\} but, because of the way we interpret external choice as an operator over distributions of states in a pLTS, it turns out that ⟦R_{2}⟧ = ⟦((a □ a)_{\frac{1}{2}} ⊕ (a □ b))_{\frac{1}{2}} ⊕ ((b □ a)_{\frac{1}{2}} ⊕ (b □ b))⟧ and so Apply(a.ω, R_{2}) = \{\frac{3}{4}\}. Therefore R_{2} ⋢_{pmay} R_{1} and R_{2} ⋢_{pmust} R_{1}.

Example 4.5 The axiom P_{p}⊕ (Q ⊓ R) = (P_{p}⊕ Q) ⊓ (P_{p}⊕ R) is unsound.

Consider the processes R_{1} = a _{\frac{1}{2}} ⊕ (b ⊓ c) and R_{2} = (a _{\frac{1}{2}} ⊕ b) ⊓ (a _{\frac{1}{2}} ⊕ c), and the test T_{1} = a.ω ⊓ (b.ω _{\frac{1}{2}} ⊕ c.ω). In the best of possible worlds, when we apply T_{1} to R_{1} we obtain probability 1, that is max(Apply(T_{1}, R_{1})) = 1. Informally this is because half the time when it is applied to the subprocess a of R_{1}, optimistically the sub-test a.ω is actually run. The other half of the time, when it is applied to the subprocess (b ⊓ c), optimistically the sub-test T_{r} = (b.ω _{\frac{1}{2}} ⊕ c.ω) is actually used. And here again, optimistically, we obtain probability 1: whenever the test b.ω is used it might be applied to the subprocess b, while when c.ω is used it might be applied to c. Formally we have

Apply(T_{1}, R_{1}) = \frac{1}{2} · Apply(T_{1}, a) + \frac{1}{2} · Apply(T_{1}, b ⊓ c)
= \frac{1}{2} · (Apply(a.ω, a) ∪ Apply(T_{r}, a)) +

\frac{1}{2} ·(Apply(T_{1}, b) ∪ Apply(T_{1}, c) ∪ Apply(a.ω, b ⊓ c) ∪ Apply(T_{r}, b ⊓ c))

= \frac{1}{2} · (\{1\} ∪ \{0\}) + \frac{1}{2} · (\{0, \frac{1}{2}\} ∪ \{0, \frac{1}{2}\} ∪ \{0\} ∪ \{0, \frac{1}{2}, 1\})
= \{0, \frac{1}{4}, \frac{1}{2}, \frac{3}{4}, 1\}

However no matter how optimistic we are when applying T_{1} to R_{2} we can never get probability 1; the most we can hope for is \frac{3}{4}, which might occur when T_{1} is applied to the subprocess (a _{\frac{1}{2}} ⊕ b). Specifically when the subprocess a is being tested the sub-test a.ω might be used, giving probability 1, and when the subprocess b is being tested the sub-test (b.ω _{\frac{1}{2}} ⊕ c.ω) might be used, giving probability \frac{1}{2}. We leave the reader to check that formally

Apply(T_{1}, R_{2}) = \{0, \frac{1}{4}, \frac{1}{2}, \frac{3}{4}\}

from which we can conclude R_{1} ⋢_{pmay} R_{2}.

We can also show that R_{2} ⋢_{pmust} R_{1}, using the test

T_{2} = (b.ω □ c.ω) ⊓ (a.ω_{\frac{1}{3}} ⊕ (b.ω_{\frac{1}{2}} ⊕ c.ω)).

Reasoning pessimistically, the worst that can happen when applying T_{2} to R_{1} is we get probability 0. Each time the subprocess a is tested the worst probability will occur when the sub-test (b.ω □ c.ω) is used; this results in probability 0. Similarly when the subprocess (b ⊓ c) is being tested the subtest (a.ω _{\frac{1}{3}} ⊕ (b.ω _{\frac{1}{2}} ⊕ c.ω)) will give probability 0. In other words min(Apply(T_{2}, R_{1})) = 0. When applying T_{2} to R_{2}, things can never be as bad. The worst probability will occur when T_{2} is applied to the subprocess (a_{\frac{1}{2}} ⊕ b), namely probability \frac{1}{6}. We leave the reader to check that formally Apply(T_{2}, R_{1}) = \{0, \frac{1}{6}, \frac{1}{3}, \frac{1}{2}, \frac{2}{3}\} and Apply(T_{2}, R_{2}) = \{\frac{1}{6}, \frac{1}{3}, \frac{1}{2}, \frac{2}{3}\}.

Example 4.6 The axiom P ⊓ (Q_{p}⊕ R) = (P ⊓ Q)_{p}⊕ (P ⊓ R) is unsound.

Let R_{1} = a ⊓ (b_{\frac{1}{2}} ⊕ c), R_{2} = (a ⊓ b)_{\frac{1}{2}} ⊕ (a ⊓ c) and T = a.(ω_{\frac{1}{2}} ⊕ 0) □ b.ω. One can check that Apply(T, R_{1}) = \{\frac{1}{2}\} and Apply(T, R_{2}) = \frac{1}{2}\{\frac{1}{2}, 1\} + \frac{1}{2}\{\frac{1}{2}, 0\} = \{\frac{1}{4}, \frac{1}{2}, \frac{3}{4}\}. Therefore we have R_{2} ⋢_{pmay} R_{1} and R_{1} ⋢_{pmust} R_{2}.

Example 4.7 The axiom P □ (Q ⊓ R) = (P □ Q) ⊓ (P □ R) is unsound.

Let R_{1} = (a _{\frac{1}{2}} ⊕ b) □ (c ⊓ d), R_{2} = ((a _{\frac{1}{2}} ⊕ b) □ c) ⊓ ((a _{\frac{1}{2}} ⊕ b) □ d) and T = (a.ω _{\frac{1}{2}} ⊕ c.ω) ⊓ (b.ω _{\frac{1}{2}} ⊕ d.ω). This time we get Apply(T, R_{1}) = \{0, \frac{1}{4}, \frac{1}{2}, \frac{3}{4}, 1\} and Apply(T, R_{2}) = \{\frac{1}{4}, \frac{3}{4}\}. So R_{1} ⋢_{pmay} R_{2} and R_{2} ⋢_{pmust} R_{1}.

Example 4.8 The axiom P ⊓ (Q □ R) = (P ⊓ Q) □ (P ⊓ R) is unsound.

Let R_{1} = (a_{\frac{1}{2}} ⊕ b) ⊓ ((a_{\frac{1}{2}} ⊕ b) □ 0) and R_{2} = ((a_{\frac{1}{2}} ⊕ b) ⊓ (a_{\frac{1}{2}} ⊕ b)) □ ((a_{\frac{1}{2}} ⊕ b) ⊓ 0). One obtains Apply(a.ω, R_{1}) = \{\frac{1}{2}\} and Apply(a.ω, R_{2}) = \{\frac{1}{2}, \frac{3}{4}\}. So R_{2} ⋢_{pmay} R_{1}. Let R_{3} and R_{4} result from substituting a_{\frac{1}{2}} ⊕ b for each of P, Q and R in the axiom above. Now Apply(a.ω, R_{3}) = \{\frac{1}{2}, \frac{3}{4}\} and Apply(a.ω, R_{4}) = \{\frac{3}{4}\}. So R_{4} ⋢_{pmust} R_{3}.

Example 4.9 The axiom P_{p}⊕ (Q □ R) = (P_{p}⊕ Q) □ (P_{p}⊕ R) is unsound.

Let R_{1} = a _{\frac{1}{2}} ⊕ (b □ c), R_{2} = (a _{\frac{1}{2}} ⊕ b) □ (a _{\frac{1}{2}} ⊕ c) and R_{3} = (a □ b) _{\frac{1}{2}} ⊕ (a □ c). R_{1} is an instance of the left-hand side of the axiom, and R_{2} an instance of the righthand side. Here we use R_{3} as a tool to reason about R_{2}, but in Section 8 we need R_{3} in its own right. Note that ⟦R_{2}⟧ = \frac{1}{2} · ⟦R_{1}⟧ + \frac{1}{2} · ⟦R_{3}⟧. Let T = a.ω. It is easy to see that Apply(T, R_{1}) = \{\frac{1}{2}\} and Apply(T, R_{3}) = \{1\}. Therefore Apply(T, R_{2}) = \{\frac{3}{4}\}. So we have R_{2} ⋢_{pmay} R_{1} and R_{2} ⋢_{pmust} R_{1}.

Of all the examples in this section, this is the only one for which we can show that ⊑_{pmay} and ⊒_{pmay} both fail, i.e. both inequations that can be associated with the axiom are unsound for may testing. Let T = a.(ω _{\frac{1}{2}} ⊕ 0) ⊓ (b.ω _{\frac{1}{2}} ⊕ c.ω). It is not hard to check that Apply(T, R_{1}) = \{0, \frac{1}{4}, \frac{1}{2}, \frac{3}{4}\} and Apply(T, R_{3}) = \{\frac{1}{2}\}. Thus Apply(T, R_{2}) = \{\frac{1}{4}, \frac{3}{8}, \frac{1}{2}, \frac{5}{8}\}. Therefore, we have R_{1} ⋢_{pmay} R_{2}.

For future reference, we also observe that R_{1} ⋢_{pmay} R_{3} and R_{3} ⋢_{pmay} R_{1}.

5 Must versus may testing

On pCSP there are two differences between the preorders ⊑_{pmay} and ⊑_{pmust}:

• Must testing is more discriminating

• The preorders ⊑_{pmay} and ⊑_{pmust} are oriented in opposite directions.

In this section we substantiate these claims by proving that P ⊑_{pmust} Q implies Q ⊑_{pmay} P, and by providing a counterexample that shows the implication is strict. We are only able to obtain the implication since our language does not feature divergence, infinite sequences of τ-actions. It is well known from the non-probabilistic theory of testing [DH84,Hen88] that in the presence of divergence ≃_{may} and ≃_{must} are incomparable.

To establish a relationship between must testing and may testing, we define the context C[ ] = |_{{ω}} (ω □ (ν ⊓ ν)) so that for every test T we obtain a new test C[T], by considering ν instead of ω as success action.

Lemma 5.1 For any process P and test T, it holds that

(i) if p ∈ Apply(T, P) then (1−p) ∈ Apply(C[T], P) (ii) if p ∈ Apply(C[T], P) then there exists a q ∈ Apply(T, P) such that 1−q ≤ p.

Proof. A state of the form C[s] |_{Act} t can always do a τ-move, and never directly a success action ν. The τ-steps that C[s] |_{Act} t can do fall into three classes: the resulting distribution is either

• a point distribution \overline{v} with v ⟶^{ν}; we call this a successful τ-step, because it contributes 1 to the set Results(C[s] |_{Act} t)

• a point distribution \overline{u} with u a state from which the success action ν is unreachable; we call this an unsuccessful τ-step, because it contributes 0 to the set Results(C[s] |_{Act} t)

• or a distribution of form C[Θ] |_{Act} Δ.

Note that

• C[s] |_{Act} t can always do a successful τ-step

• C[s] |_{Act} t can do an unsuccessful τ-step iff s |_{Act} t can do a ω-step

• and C[s] |_{Act} t ⟶^{τ} C[Θ] |_{Act} Δ iff s |_{Act} t ⟶^{τ} Θ |_{Act} Δ.

Using this, both claims follow by a straightforward induction on T and P. □

Proposition 5.2 If P ⊑_{pmust} Q then Q ⊑_{pmay} P.

Proof. Suppose P ⊑_{pmust} Q. We must show that, for any test T, if p ∈ Apply(T, Q) then there exists a q ∈ Apply(T, P) such that p ≤ q. So suppose p ∈ Apply(T, Q). By the first clause of Lemma 5.1, we have (1−p) ∈ Apply(C[T], Q). Given that P ⊑_{pmust} Q, there must be an x ∈ Apply(C[T], P) such that x ≤ 1−p. By the second clause of Lemma 5.1, there exists a q ∈ Apply(T, P) such that 1−q ≤ x. It follows that p ≤ q. Therefore Q ⊑_{pmay} P. □

Example 5.3 To show that must testing is strictly more discriminating than may testing consider the processes a □ b and a ⊓ b, and expose them to test a.ω. It is not hard to see that Apply(a.ω, a □ b) = {1}, whereas Apply(a.ω, a ⊓ b) = {0, 1}. Since min(Apply(a.ω, a □ b)) = 1 and min(Apply(a.ω, a ⊓ b)) = 0, using Proposition 2.1 we obtain that (a □ b) ⋢_{pmust} (a ⊓ b).

Since max(Apply(a.ω, a □ b)) = max(Apply(a.ω, a ⊓ b)) = 1, as a may test, the test a.ω does not differentiate between a □ b and a ⊓ b. In fact, we have (a ⊓ b) ⊑_{pmay} (a □ b), and even (a □ b) ≃_{pmay} (a ⊓ b), but this cannot be shown so easily, as we would have to consider all possible tests. In Section 6 we will develop a tool to prove statements P ⊑_{pmay} Q, and apply it to derive the equality above (axiom (EI) in Figure 8).

6 Simulations

The examples of Section 4 have been all negative, because one can easily demonstrate an inequivalence between two processes by exhibiting a test which distinguishes them in the appropriate manner. A direct application of the definition of the testing preorders is usually unsuitable for establishing positive results, as this involves a universal quantification over all possible tests that can be applied. To give positive results of the form P ⊑_{pmay} Q (and similarly for P ⊑_{pmust} Q) we need to come up with a preorder ⊑_{finer} such that (P ⊑_{finer} Q) ⇒ (P ⊑_{pmay} Q) and statements P ⊑_{finer} Q can be obtained by exhibiting a single witness.

In this section we report on investigations in this direction, using simulations as our witnesses. We confine ourselves to may testing, although similar results hold for must testing. The definitions are somewhat complicated by the fact that in a pLTS transitions go from states to distributions; consequently if we are to use sequences of transitions, or weak transitions ⟹^{a} which abstract from sequences of internal actions that might precede or follow the a-transition, then we need to generalise transitions so that they go from distributions to distributions. We first develop the mathematical machinery for doing this.

6.1 Lifting relations

Let R ⊆ S × D(S) be a relation from states to distributions. We lift it to a relation \overline{R} ⊆ D(S) × D(S) by letting Δ_{1} \overline{R} Δ_{2} whenever

(i) Δ_{1} = ∑_{i∈I} p_{i} · \overline{s_{i}}, where I is a finite index set and ∑_{i∈I} p_{i} = 1 (ii) For each i ∈ I there is a distribution Φ_{i} such that s_{i} R Φ_{i} (iii) Δ_{2} = ∑_{i∈I} p_{i} · Φ_{i}.

An important point here is that in the decomposition (i) of Δ_{1} into ∑_{i∈I} p_{i} · \overline{s_{i}}, the states s_{i} are not necessarily distinct: that is, the decomposition is not in general unique. Thus when establishing the relationship between Δ_{1} and Δ_{2}, a given state s in Δ_{1} may play a number of different roles, and this is seen clearly if we apply this definition to the action relations ⟶^{α} ⊆ S_{p} × D(S_{p}) in the operational semantics of pCSP. We obtain lifted relations between D(S_{p}) and D(S_{p}), which to ease the notation we write as Δ_{1} ⟶^{α} Δ_{2}; then, using pCSP terms to represent distributions, a simple instance of a transition between distributions is given by

(a.b □ a.c)_{\frac{1}{2}} ⊕ a.d ⟶^{a} b_{\frac{1}{2}} ⊕ d

But we also have

(a.b □ a.c)_{\frac{1}{2}} ⊕ a.d ⟶^{a} (b_{\frac{1}{2}} ⊕ c)_{\frac{1}{2}} ⊕ d  (1)

because, viewed as a distribution, the term (a.b □ a.c)_{\frac{1}{2}} ⊕ a.d may be re-written as ((a.b □ a.c)_{\frac{1}{2}} ⊕ (a.b □ a.c)) _{\frac{1}{2}} ⊕ a.d representing the sum of point distributions

\frac{1}{4} · \overline{(a.b □ a.c)} + \frac{1}{4} · \overline{(a.b □ a.c)} + \frac{1}{2} · \overline{a.d}

from which the move (1) can easily be derived using the three moves from states

a.b □ a.c ⟶^{a} \overline{b}  a.b □ a.c ⟶^{a} \overline{c}  a.d ⟶^{a} \overline{d}

The lifting construction satisfies the following two useful properties, whose proofs we leave to the reader.

Proposition 6.1 Suppose R ⊆ S × D(S) and ∑_{i∈I} p_{i} = 1. Then we have

(i) Θ_{i} \overline{R} Δ_{i} implies (∑_{i∈I} p_{i} · Θ_{i}) \overline{R} (∑_{i∈I} p_{i} · Δ_{i}). (ii) If (∑_{i∈I} p_{i} · Θ_{i}) \overline{R} Δ then Δ = ∑_{i∈I} p_{i} · Δ_{i} for some set of distributions Δ_{i}

such that Θ_{i} \overline{R} Δ_{i}. □

The lifting construction can also be used to define the concept of a partial internal move between distributions, one where part of the distribution does an internal move and the remainder remains unchanged. Write s ⟶^{τ̂} Δ if either s ⟶^{τ} Δ or Δ = \overline{s}. This relation between states and distributions can be lifted to one between distributions and distributions, and again for notational convenience we use Δ_{1} ⟶^{τ̂} Δ_{2} to denote the lifted relation. As an example, again using process terms to denote distributions, we have

(a ⊓ b)_{\frac{1}{2}} ⊕ (a ⊓ c) ⟶^{τ̂} a_{\frac{1}{2}} ⊕ (a ⊓ b _{\frac{1}{2}} ⊕ c)

This follows because as a distribution (a ⊓ b)_{\frac{1}{2}} ⊕ (a ⊓ c) may be written as

\frac{1}{4} · \overline{(a ⊓ b)} + \frac{1}{4} · \overline{(a ⊓ b)} + \frac{1}{4} · \overline{(a ⊓ c)} + \frac{1}{4} · \overline{(a ⊓ c)}

and we have the four moves from states to distributions:

(a ⊓ b) ⟶^{τ̂} \overline{a}  (a ⊓ b) ⟶^{τ̂} \overline{(a ⊓ b)}
(a ⊓ c) ⟶^{τ̂} \overline{a}  (a ⊓ c) ⟶^{τ̂} \overline{c}

6.2 The simulation preorder

Following tradition it would be natural to define simulations as relations between states in a pLTS [JWL01,SL94]. However, technically it is more convenient to use relations in S_{p} ↔ D(S_{p}). One reason may be understood through the example in Figure 5. Although in Example 4.1 we found that R_{2} ⋢_{pmay} R_{1}, we do have R_{1} ⊑_{pmay} R_{2}. If we are to relate these processes via a simulation-like relation, then the initial state of R_{1} needs to be related to the initial distribution of R_{2}, containing the two states a.b and a.c.

Our definition of simulation uses weak transitions [Mil89], which have the standard definitions except that they now apply to distributions, and ⟶^{τ̂} is used instead of ⟶^{τ}. This reflects the understanding that if a distribution may perform a sequence of internal moves before or after executing a visible action, different parts of the distribution may perform different numbers of internal actions:

• Let Δ_{1} ⟹^{τ̂} Δ_{2} whenever Δ_{1} ⟶^{τ̂}^{∗} Δ_{2}.

• Similarly Δ_{1} ⟹^{â} Δ_{2} denotes Δ_{1} ⟶^{τ̂}^{∗} ⟶^{a} ⟶^{τ̂}^{∗} Δ_{2} whenever a ∈ Act.

Definition 6.2 [Seg95] A relation R ⊆ S_{p} × D(S_{p}) is said to be a simulation if for all s, Δ, α, Θ we have that s R Δ and s ⟶^{α} Θ implies there exists some Δ′ with

Δ ⟹^{α̂} Δ′ and Θ \overline{R} Δ′.

We write s ⊳_{S} Δ to mean that there is some simulation R such that s R Δ. Note that the lifting operation on relations is monotone, in the sense that R ⊆ S implies \overline{R} ⊆ \overline{S}. Hence ⊳_{S}, which is the union of all simulations, is a simulation itself. Therefore, ⊳_{S} could just as well have been defined co-inductively as the largest relation ⊳_{S} ⊆ S_{p} × D(S_{p}) satisfying, for all s ∈ S_{p}, Δ ∈ D(S_{p}) and α ∈ Act_{τ},

s R Δ ∧ s ⟶^{α} Θ ⇒ ∃Δ′. Δ ⟹^{α̂} Δ′ ∧ Θ \overline{R} Δ′

Definition 6.3 The simulation preorder on process terms is defined by letting P ⊑_{S} Q whenever there is a distribution Δ with ⟦Q⟧ ⟹^{τ̂} Δ and ⟦P ⟧ \overline{⊳_{S}} Δ. The symmetric closure of ⊑_{S} is denoted ≃_{S}.

\begin{matrix}s_{0} ; \begin{matrix}Δ_{1} \\ a \end{matrix} ; _{s_{1}_{\frac{1}{2}} ; b s_{2}_{\frac{1}{4}} ; c s_{3}_{\frac{1}{4}} ; c} & t_{0} ; \begin{matrix}Δ_{2} \\ a \end{matrix} ; _{t_{1}_{\frac{1}{4}} ; b t_{2}_{\frac{1}{4}} ; b t_{3}_{\frac{1}{2}} ; c} \\ P_{1} = a.(b_{\frac{1}{2}} ⊕ (c_{\frac{1}{2}} ⊕ c)) & P_{2} = a.((b_{\frac{1}{2}} ⊕ b)_{\frac{1}{2}} ⊕ c) \end{matrix}

Fig. 7. Two simulation equivalent processes

If P ∈ S_{p}, that is if P is a state in the pLTS of pCSP and so ⟦P ⟧ = \overline{P}, then to establish P ⊑_{S} Q it is sufficient to exhibit a simulation between the state P and the distribution ⟦Q⟧, because trivially s ⊳_{S} Δ implies \overline{s} \overline{⊳_{S}} Δ.

Example 6.4 Consider the two processes P_{i} in Figure 7. To show P_{1} ⊑_{S} P_{2} it is sufficient to exhibit a simulation R such that s_{0} R \overline{t_{0}}. Let R ⊆ S_{p} × D(S_{p}) be defined by

s_{0} R \overline{t_{0}}  s_{1} R Δ_{t}  s_{2} R \overline{t_{3}}  s_{3} R \overline{t_{3}}  0 R \overline{0}

where Δ_{t} is the two-point distribution mapping both t_{1} and t_{2} to the probability \frac{1}{2}. Then it is straightforward to check that it satisfies the requirements of a simulation: the only non-trivial requirement is that Δ_{1} \overline{R} Δ_{2}. But this follows from the fact that

Δ_{1} = \frac{1}{2} · \overline{s_{1}} + \frac{1}{4} · \overline{s_{2}} + \frac{1}{4} · \overline{s_{3}}
Δ_{2} = \frac{1}{2} · Δ_{t} + \frac{1}{4} · \overline{t_{3}} + \frac{1}{4} · \overline{t_{3}}

As another example reconsider R_{1} = a.(b_{\frac{1}{2}} ⊕ c) and R_{2} = a.b_{\frac{1}{2}} ⊕ a.c from Figure 5, where for convenience we use process terms to denote their semantic interpretations. It is easy to see that R_{1} ⊑_{S} R_{2} because of the simulation

R_{1} R ⟦R_{2}⟧  b R \overline{b}  c R \overline{c}  0 R \overline{0}

Namely R_{2} ⟶^{a} (b_{\frac{1}{2}} ⊕ c) and (b_{\frac{1}{2}} ⊕ c) \overline{R} (b_{\frac{1}{2}} ⊕ c).

Similarly (a _{\frac{1}{2}} ⊕ c) ⊓ (b _{\frac{1}{2}} ⊕ c) ⊑_{S} (a ⊓ b) _{\frac{1}{2}} ⊕ c because it is possible to find a simulation between the state (a_{\frac{1}{2}} ⊕ c) ⊓ (b_{\frac{1}{2}} ⊕ c) and the distribution (a ⊓ b)_{\frac{1}{2}} ⊕ c.

In case P ∉ S_{p}, a statement P ⊑_{S} Q cannot always be established by a simulation R such that ⟦P ⟧ \overline{R} ⟦Q⟧.

Example 6.5 Compare the processes P = a _{\frac{1}{2}} ⊕ b and P ⊓ P. Note that ⟦P ⟧ is the distribution \frac{1}{2} \overline{a} +\frac{1}{2} \overline{b} whereas ⟦P ⊓ P ⟧ is the point distribution \overline{P ⊓ P}. The relation R given by

(P ⊓ P) R (\frac{1}{2} \overline{a} +\frac{1}{2} \overline{b})  a R \overline{a}  b R \overline{b}  0 R \overline{0}

is a simulation, because the τ-step P ⊓ P ⟶^{τ} (\frac{1}{2} \overline{a} +\frac{1}{2} \overline{b}) can be matched by the idle transition (\frac{1}{2} \overline{a} +\frac{1}{2} \overline{b}) ⟹^{τ̂} (\frac{1}{2} \overline{a} +\frac{1}{2} \overline{b}), and we have (\frac{1}{2} \overline{a} +\frac{1}{2} \overline{b}) \overline{R} (\frac{1}{2} \overline{a} +\frac{1}{2} \overline{b}). Thus (P ⊓ P) ⊳_{S} (\frac{1}{2} \overline{a} +\frac{1}{2} \overline{b}) = ⟦P ⟧, hence ⟦P ⊓ P ⟧ \overline{⊳_{S}} ⟦P ⟧, and therefore P ⊓ P ⊑_{S} P.

This type of reasoning does not apply to the other direction. Any simulation R with (\frac{1}{2} \overline{a} +\frac{1}{2} \overline{b}) \overline{R} \overline{P ⊓ P} would have to satisfy a R \overline{P ⊓ P} and b R \overline{P ⊓ P}. However, the move a ⟶^{a} 0 cannot be matched by the process \overline{P ⊓ P}, as the only transition the latter process can do is \overline{P ⊓ P} ⟶^{τ} (\frac{1}{2} \overline{a} +\frac{1}{2} \overline{b}), and only half of that distribution can match the a-move. Thus, no such simulation exists, and we find ⟦P ⟧ \overline{⋫_{S}} ⟦P ⊓ P ⟧. Nevertheless, we still have P ⊑_{S} P ⊓ P. Here, the transition ⟹^{τ̂} from Definition 6.3 comes to the rescue. As ⟦P ⊓ P ⟧ ⟹^{τ̂} ⟦P ⟧ and ⟦P ⟧ \overline{⊳_{S}} ⟦P ⟧, we obtain P ⊑_{S} P ⊓ P.

Because of the asymmetric use of distributions in the definition of simulation it is not immediately obvious that ⊑_{S} is actually a preorder (a reflexive and transitive relation) and hence ≃_{S} an equivalence relation. In order to show this, we first need to establish some properties of ⊳_{S}.

Lemma 6.6 Suppose ∑_{i∈I} p_{i} = 1 and Δ_{i} ⟹^{α̂} Φ_{i} for each i ∈ I, with I a finite index set. (Recall that ∑_{i∈I} p_{i} · Δ_{i} is only defined for finite I.) Then

∑_{i∈I} p_{i} · Δ_{i} ⟹^{α̂} ∑_{i∈I} p_{i} · Φ_{i}

Proof. We first prove the case α = τ. For each i ∈ I there is a number k_{i} such

that Δ_{i} = Δ_{i0} ⟶^{τ̂} Δ_{i1} ⟶^{τ̂} Δ_{i2} ⟶^{τ̂} ⋯ ⟶^{τ̂} Δ_{ik_{i}} = Δ′_{i}. Let k = max{k_{i} | i ∈ I},

using that I is finite. Since we have Φ ⟶^{τ̂} Φ for any Φ ∈ D(S), we can add spurious transitions to these sequences, until all k_{i} equal k. After this preparation the lemma follows by k applications of Proposition 6.1(i), taking ⟶^{τ̂} for R.

The case α ∈ Act now follows by one more application of Proposition 6.1(i), this time with R = ⟶^{a}, preceded and followed by an application of the case α = τ. □

Lemma 6.7 Suppose Δ \overline{⊳_{S}} Φ and Δ ⟶^{α} Δ′. Then Φ ⟹^{α̂} Φ′ for some Φ′ such that Δ′ \overline{⊳_{S}} Φ′.

Proof. First Δ \overline{⊳_{S}} Φ means that

Δ = ∑_{i∈I} p_{i} · \overline{s_{i}},  s_{i} ⊳_{S} Φ_{i},  Φ = ∑_{i∈I} p_{i} · Φ_{i} ;  (2)

also Δ ⟶^{α} Δ′ means

Δ = ∑_{j∈J} q_{j} · \overline{t_{j}},  t_{j} ⟶^{α} Θ_{j},  Δ′ = ∑_{j∈J} q_{j} · Θ_{j} ,  (3)

and we can assume w.l.o.g. that all the coefficients p_{i}, q_{j} are non-zero. Now define I_{j} = { i ∈ I | s_{i} = t_{j} } and J_{i} = { j ∈ J | t_{j} = s_{i} }, so that trivially

{(i, j) | i ∈ I, j ∈ J_{i}}  =  {(i, j) | j ∈ J, i ∈ I_{j}}  (4)

and note that

Δ(s_{i}) = ∑_{j∈J_{i}} q_{j}  and  Δ(t_{j}) = ∑_{i∈I_{j}} p_{i}  (5)

Because of (5) we have

Φ = ∑_{i∈I} p_{i} · Φ_{i} = ∑_{i∈I} p_{i} · ∑_{j∈J_{i}} \frac{q_{j}}{Δ(s_{i})} · Φ_{i}

= ∑_{i∈I} ∑_{j∈J_{i}} \frac{p_{i} · q_{j}}{Δ(s_{i})} · Φ_{i}

Now for each j in J_{i} we know that in fact t_{j} = s_{i}, and so from the middle parts of (2) and (3) we obtain Φ_{i} ⟹^{α̂} Φ_{ij} such that Θ_{j} \overline{⊳_{S}} Φ_{ij}. Lemma 6.6 yields

Φ ⟹^{α̂} Φ′ = ∑_{i∈I} ∑_{j∈J_{i}} \frac{p_{i} · q_{j}}{Δ(s_{i})} · Φ_{ij}

where within the summations s_{i} = t_{j}, so that, using (4), Φ′ can also be written as

∑_{j∈J} ∑_{i∈I_{j}} \frac{p_{i} · q_{j}}{Δ(t_{j})} · Φ_{ij}  (6)

All that remains is to show that Δ′ \overline{⊳_{S}} Φ′, which we do by manipulating Δ′ so that it takes on a form similar to that in (6):

Δ′ = ∑_{j∈J} q_{j} · Θ_{j}

= ∑_{j∈J} q_{j} · ∑_{i∈I_{j}} \frac{p_{i}}{Δ(t_{j})} · Θ_{j} using (5) again

= ∑_{j∈J} ∑_{i∈I_{j}} \frac{p_{i} · q_{j}}{Δ(t_{j})} · Θ_{j}

Comparing this with (6) above we see that the required result, Δ′ \overline{⊳_{S}} Φ′, follows from an application of Proposition 6.1(i). □

Lemma 6.8 Suppose Δ \overline{⊳_{S}} Φ and Δ ⟹^{α̂} Δ′. Then Φ ⟹^{α̂} Φ′ for some Φ′ such that Δ′ \overline{⊳_{S}} Φ′.

Proof. First we consider two claims

(i) If Δ \overline{⊳_{S}} Φ and Δ ⟶^{τ̂} Δ′, then Φ ⟹^{τ̂} Φ′ for some Φ′ such that Δ′ \overline{⊳_{S}} Φ′. (ii) If Δ \overline{⊳_{S}} Φ and Δ ⟹^{τ̂} Δ′, then Φ ⟹^{τ̂} Φ′ for some Φ′ such that Δ′ \overline{⊳_{S}} Φ′.

The proof of claim (i) is similar to the proof of Lemma 6.7. Claim (ii) follows from claim (i) by induction on the length of the derivation of ⟹^{τ̂}. By combining claim (ii) with Lemma 6.7, we obtain the required result. □

Proposition 6.9 The relation \overline{⊳_{S}} is both reflexive and transitive on distributions.

Proof. We leave reflexivity to the reader; it relies on the fact that s ⊳_{S} \overline{s} for every state s.

For transitivity, let R ⊆ S_{p} × D(S_{p}) be given by s R Φ iff s ⊳_{S} Δ \overline{⊳_{S}} Φ for some intermediate distribution Δ. Transitivity follows from the two claims

(i) Θ \overline{⊳_{S}} Δ \overline{⊳_{S}} Φ implies Θ \overline{R} Φ (ii) R is a simulation, hence \overline{R} ⊆ \overline{⊳_{S}}.

Claim (ii) is a straightforward application of Lemma 6.8, so let us look at (i). From Θ \overline{⊳_{S}} Δ we have

Θ = ∑_{i∈I} p_{i} · \overline{s_{i}},  s_{i} ⊳_{S} Δ_{i},  Δ = ∑_{i∈I} p_{i} · Δ_{i}

Since Δ \overline{⊳_{S}} Φ, from part (ii) of Proposition 6.1 we know Φ = ∑_{i∈I} p_{i} · Φ_{i} such that Δ_{i} \overline{⊳_{S}} Φ_{i}. So for each i we have s_{i} R Φ_{i}, from which it follows that Θ \overline{R} Φ. □

Corollary 6.10 ⊑_{S} is a preorder, i.e. it is reflexive and transitive.

Proof. By combination of Lemma 6.8 and Proposition 6.9. □

6.3 The simulation preorder is a precongruence

In Theorem 6.13 of this section we establish that the pCSP operators are monotone w.r.t. the simulation preorder ⊑_{S}, i.e. that ⊑_{S} is a precongruence for pCSP. This implies that the pCSP operators are compositional for ≃_{S} or, equivalently, that ≃_{S} is a congruence for pCSP. The following two lemmas gather some facts we need in the proof of this theorem. Their proofs are straightforward, although somewhat tedious.

Lemma 6.11 (i) If Φ ⟹^{τ̂} Φ′ then Φ □ Δ ⟹^{τ̂} Φ′ □ Δ and Δ □ Φ ⟹^{τ̂} Δ □ Φ′. (ii) If Φ ⟶^{a} Φ′ then Φ □ Δ ⟶^{a} Φ′ and Δ □ Φ ⟶^{a} Φ′. (iii) (∑_{j∈J} p_{j} · Φ_{j}) □ (∑_{k∈K} q_{k} · Δ_{k}) = ∑_{j∈J} ∑_{k∈K}(p_{j} · q_{k}) · (Φ_{j} □ Δ_{k}). (iv) Given relations R, R′ ⊆ S_{p} × D(S_{p}) satisfying sR′Δ whenever s = s_{1} □ s_{2} and

Δ = Δ_{1} □ Δ_{2} with s_{1} R Δ_{1} and s_{2} R Δ_{2}. Then Φ_{i} \overline{R} Δ_{i} for i = 1, 2 implies (Φ_{1} □ Φ_{2}) \overline{R′} (Δ_{1} □ Δ_{2}). □

Lemma 6.12 (i) If Φ ⟹^{τ̂} Φ′ then Φ |_{A} Δ ⟹^{τ̂} Φ′ |_{A} Δ and Δ |_{A} Φ ⟹^{τ̂} Δ |_{A} Φ′. (ii) If Φ ⟶^{a} Φ′ and a ∉ A then Φ |_{A} Δ ⟶^{a} Φ′ |_{A} Δ and Δ |_{A} Φ ⟶^{a} Δ |_{A} Φ′. (iii) If Φ ⟶^{a} Φ′, Δ ⟶^{a} Δ′ and a ∈ A then Δ |_{A} Φ ⟶^{τ} Δ′ |_{A} Φ′. (iv) (∑_{j∈J} p_{j} · Φ_{j}) |_{A} (∑_{k∈K} q_{k} · Δ_{k}) = ∑_{j∈J} ∑_{k∈K}(p_{j} · q_{k}) · (Φ_{j} |_{A} Δ_{k}).

(v) Given relations R, R′ ⊆ S_{p} × D(S_{p}) satisfying sR′Δ whenever s = s_{1} |_{A} s_{2} and Δ = Δ_{1} |_{A} Δ_{2} with s_{1} R Δ_{1} and s_{2} R Δ_{2}. Then Φ_{i} \overline{R} Δ_{i} for i = 1, 2 implies (Φ_{1} |_{A} Φ_{2}) \overline{R′} (Δ_{1} |_{A} Δ_{2}). □

Theorem 6.13 Suppose P_{i} ⊑_{S} Q_{i} for i = 1, 2. Then

(i) a.P_{1} ⊑_{S} a.Q_{1} (ii) P_{1} ⊓ P_{2} ⊑_{S} Q_{1} ⊓ Q_{2} (iii) P_{1} □ P_{2} ⊑_{S} Q_{1} □ Q_{2} (iv) P_{1}_{p}⊕ P_{2} ⊑_{S} Q_{1}_{p}⊕ Q_{2}

(v) P_{1} |_{A} P_{2} ⊑_{S} Q_{1} |_{A} Q_{2}

Proof.

(i) Since P_{1} ⊑_{S} Q_{1}, there must be a Δ_{1} such that ⟦Q_{1}⟧ ⟹^{τ̂} Δ_{1} and ⟦P_{1}⟧ \overline{⊳_{S}} Δ_{1}. It is easy to see that a.P_{1} ⊳_{S} \overline{a.Q_{1}} because the transition a.P_{1} ⟶^{a} ⟦P_{1}⟧ can be

matched by \overline{a.Q_{1}} ⟶^{a} ⟦Q_{1}⟧ ⟹^{τ̂} Δ_{1}. Thus ⟦a.P_{1}⟧ = \overline{a.P_{1}} \overline{⊳_{S}} \overline{a.Q_{1}} = ⟦a.Q_{1}⟧.

(ii) Since P_{i} ⊑_{S} Q_{i}, there must be a Δ_{i} such that ⟦Q_{i}⟧ ⟹^{τ̂} Δ_{i} and ⟦P_{i}⟧ \overline{⊳_{S}} Δ_{i}. It is easy to see that P_{1} ⊓ P_{2} ⊳_{S} \overline{Q_{1} ⊓ Q_{2}} because the transition P_{1} ⊓ P_{2} ⟶^{τ} ⟦P_{i}⟧, for i = 1 or i = 2, can be matched by \overline{Q_{1} ⊓ Q_{2}} ⟶^{τ} ⟦Q_{i}⟧ ⟹^{τ̂} Δ_{i}. Thus ⟦P_{1} ⊓ P_{2}⟧ = \overline{P_{1} ⊓ P_{2}} \overline{⊳_{S}} \overline{Q_{1} ⊓ Q_{2}} = ⟦Q_{1} ⊓ Q_{2}⟧.

(iii) Let R ⊆ S_{p} × D(S_{p}) be defined by s R Δ iff either s ⊳_{S} Δ or s = s_{1} □ s_{2} and

Δ = Δ_{1} □ Δ_{2} with s_{1} ⊳_{S} Δ_{1} and s_{2} ⊳_{S} Δ_{2}. We show that R is a simulation.

Suppose s_{1} ⊳_{S} Δ_{1}, s_{2} ⊳_{S} Δ_{2} and s_{1} □ s_{2} ⟶^{a} Θ with a ∈ Act. Then s_{i} ⟶^{a} Θ for i = 1 or i = 2. Thus Δ_{i} ⟹^{â} Δ for some Δ with Θ \overline{⊳_{S}} Δ, and hence Θ \overline{R} Δ. By Lemma 6.11 we have Δ_{1} □ Δ_{2} ⟹^{â} Δ.

Now suppose s_{1} ⊳_{S} Δ_{1}, s_{2} ⊳_{S} Δ_{2} and s_{1} □ s_{2} ⟶^{τ} Θ. Then s_{1} ⟶^{τ} Φ and Θ = Φ □ \overline{s_{2}} or s_{2} ⟶^{τ} Φ and Θ = \overline{s_{1}} □ Φ. By symmetry we may restrict attention to the first case. Thus Δ_{1} ⟹^{τ̂} Δ for some Δ with Φ \overline{⊳_{S}} Δ. By Lemma 6.11 we have (Φ □ \overline{s_{2}}) \overline{R} (Δ □ Δ_{2}) and Δ_{1} □ Δ_{2} ⟹^{τ̂} Δ □ Δ_{2}.

The case that s ⊳_{S} Δ is trivial, so we have checked that R is a simulation indeed. Using this, we proceed to show that P_{1} □ P_{2} ⊑_{S} Q_{1} □ Q_{2}.

Since P_{i} ⊑_{S} Q_{i}, there must be a Δ_{i} such that ⟦Q_{i}⟧ ⟹^{τ̂} Δ_{i} and ⟦P_{i}⟧ \overline{⊳_{S}} Δ_{i}. By Lemma 6.11, we have ⟦P_{1} □ P_{2}⟧ = (⟦P_{1}⟧ □ ⟦P_{2}⟧) \overline{R} (Δ_{1} □ Δ_{2}). Therefore ⟦P_{1} □ P_{2}⟧ \overline{⊳_{S}} (Δ_{1} □ Δ_{2}). By Lemma 6.11 we also obtain ⟦Q_{1} □ Q_{2}⟧ = ⟦Q_{1}⟧ □ ⟦Q_{2}⟧ ⟹^{τ̂} Δ_{1} □ ⟦Q_{2}⟧ ⟹^{τ̂} Δ_{1} □ Δ_{2}, so the required result is established.

(iv) Since P_{i} ⊑_{S} Q_{i}, there must be a Δ_{i} such that ⟦Q_{i}⟧ ⟹^{τ̂} Δ_{i} and ⟦P_{i}⟧ \overline{⊳_{S}} Δ_{i}.

Thus ⟦Q_{1}_{p}⊕ Q_{2}⟧ = p·⟦Q_{1}⟧+(1−p)·⟦Q_{2}⟧ ⟹^{τ̂} p·Δ_{1} +(1−p)·Δ_{2} by Lemma 6.6

and ⟦P_{1}_{p}⊕ P_{2}⟧ = p·⟦P_{1}⟧+(1−p)·⟦P_{2}⟧ \overline{⊳_{S}} p·Δ_{1}+(1−p)·Δ_{2} by Proposition 6.1(i). Hence P_{1}_{p}⊕ P_{2} ⊑_{S} Q_{1}_{p}⊕ Q_{2}.

(v) Let R ⊆ S_{p} × D(S_{p}) be defined by s R Δ iff s = s_{1} |_{A} s_{2} and Δ = Δ_{1} |_{A} Δ_{2} with s_{1} ⊳_{S} Δ_{1} and s_{2} ⊳_{S} Δ_{2}. We show that R is a simulation. There are three cases to consider.

(a) Suppose s_{1} ⊳_{S} Δ_{1}, s_{2} ⊳_{S} Δ_{2} and s_{1} |_{A} s_{2} ⟶^{α} Θ_{1} |_{A} \overline{s_{2}} because of the transition s_{1} ⟶^{α} Θ_{1} with α ∉ A. Then Δ_{1} ⟹^{α̂} Δ′_{1} for some Δ′_{1} with Θ_{1} \overline{⊳_{S}} Δ′_{1}. By Lemma 6.12 we have Δ_{1} |_{A} Δ_{2} ⟹^{α̂} Δ′_{1} |_{A} Δ_{2} and also (Θ_{1} |_{A} \overline{s_{2}}) \overline{R} (Δ′_{1} |_{A} Δ_{2}).

(b) The symmetric case can be similarly analysed.

(c) Suppose s_{1} ⊳_{S} Δ_{1}, s_{2} ⊳_{S} Δ_{2} and s_{1} |_{A} s_{2} ⟶^{τ} Θ_{1} |_{A} Θ_{2} because of the transitions s_{1} ⟶^{a} Θ_{1} and s_{2} ⟶^{a} Θ_{2} with a ∈ A. Then for i = 1 and i = 2

we have Δ_{i} ⟹^{τ̂} Δ′_{i} ⟶^{a} Δ′′_{i} ⟹^{τ̂} Δ′′′_{i} for some Δ′_{i}, Δ′′_{i}, Δ′′′_{i} with Θ_{1} \overline{⊳_{S}} Δ′′′_{i}. By

Lemma 6.12 we have Δ_{1} |_{A} Δ_{2} ⟹^{τ̂} Δ′_{1} |_{A} Δ′_{2} ⟶^{τ} Δ′′_{1} |_{A} Δ′′_{2} ⟹^{τ̂} Δ′′′_{1} |_{A} Δ′′′_{2}

and (Θ_{1} |_{A} Θ_{2}) \overline{R} (Δ′′′_{1} |_{A} Δ′′′_{2}). So we have checked that R is a simulation.

Since P_{i} ⊑_{S} Q_{i}, there must be a Δ_{i} such that ⟦Q_{i}⟧ ⟹^{τ̂} Δ_{i} and ⟦P_{i}⟧ \overline{⊳_{S}} Δ_{i}. By Lemma 6.12 we have ⟦P_{1} |_{A} P_{2}⟧ = (⟦P_{1}⟧ |_{A} ⟦P_{2}⟧) \overline{R} (Δ_{1} |_{A} Δ_{2}). Therefore ⟦P_{1} |_{A} P_{2}⟧ \overline{⊳_{S}} (Δ_{1} |_{A} Δ_{2}). By Lemma 6.12 we also obtain ⟦Q_{1} |_{A} Q_{2}⟧ = ⟦Q_{1}⟧ |_{A} ⟦Q_{2}⟧ ⟹^{τ̂} Δ_{1} |_{A} ⟦Q_{2}⟧ ⟹^{τ̂} Δ_{1} |_{A} Δ_{2}, which had to be established. □

6.4 Simulation is sound for may testing

This section is devoted to the proof that P ⊑_{S} Q implies P ⊑_{pmay} Q. It involves a slightly different method of analysing the transition systems which result from applying a test to a process. Instead of collecting the set of probabilities of success it calculates the maximum probability that some action can be performed. Let maxlive : S_{p} → [0, 1] be defined by

maxlive(s) = \begin{cases}1 & if s ⟶^{a} for some a ∈ Act^{ω} \\ max(\{ maxlive(Δ) | s ⟶^{τ} Δ \}) & if s −̸→^{a} for all a ∈ Act^{ω} and s ⟶^{τ} \\ 0 & otherwise \end{cases}

where

maxlive(Δ) = ∑_{s∈⌈Δ⌉} Δ(s) · maxlive(s)

If s ∈ S_{p} only ever gives rise to the special action ω then it is easy to see that maxlive(s) = max(Results(s)). Because of this fact the following result is straightforward:

Proposition 6.14 P ⊑_{pmay} Q if and only if for every test T we have

maxlive(⟦T |_{Act} P ⟧) ≤ maxlive(⟦T |_{Act} Q⟧) □

The main technical property we require of maxlive( ) is that it does not increase as τ-transitions are performed:

Lemma 6.15 Δ_{1} ⟶^{τ̂}^{∗} Δ_{2} implies maxlive(Δ_{1}) ≥ maxlive(Δ_{2}).

Proof. First we prove one special case:

Δ_{1} ⟶^{τ̂} Δ_{2} implies maxlive(Δ_{1}) ≥ maxlive(Δ_{2}) .  (7)

We know from Δ_{1} ⟶^{τ̂} Δ_{2} that

Δ_{1} = ∑_{i∈I} p_{i} · \overline{s_{i}},  s_{i} ⟶^{τ̂} Φ_{i},  Δ_{2} = ∑_{i∈I} p_{i} · Φ_{i}  (8)

The second part of (8) means that (i) either Φ_{i} = \overline{s_{i}} or (ii) s_{i} ⟶^{τ} Φ_{i}. In case (i) we have maxlive(s_{i}) = maxlive(Φ_{i}); in case (ii) we know from the definition of maxlive( ) that maxlive(s_{i}) ≥ maxlive(Φ_{i}). Therefore,

maxlive(Δ_{1}) = ∑_{i∈I} p_{i} · maxlive(s_{i})
≥ ∑_{i∈I} p_{i} · maxlive(Φ_{i})
= maxlive(Δ_{2})

This completes the proof of (7), from which the general case follows by transition induction. □

This lemma is the main ingredient to the following result:

Proposition 6.16 Suppose R is a simulation. Then

(i) s R Δ implies maxlive(s) ≤ maxlive(Δ) (ii) Θ \overline{R} Δ implies maxlive(Θ) ≤ maxlive(Δ).

Proof. Given that the states of our pLTS are pCSP expressions, there exists a well-founded order on the combination of states in S_{p} and distributions in D(S_{p}), such that s ⟶^{α} Δ implies that s is larger than Δ, and any distribution is larger than the states in its support. We prove (i) and (ii) by simultaneous induction on this order, applied to s and Θ.

(i) We distinguish two cases.

• If s ⟶^{a} Θ for some action a ∈ Act and distribution Θ, then maxlive(s) = 1. Since s R Δ, there exists Δ′, Δ′′ such that Δ ⟶^{τ̂}^{∗} Δ′ ⟶^{a} ⟶^{τ̂}^{∗} Δ′′ and Θ \overline{R} Δ′′. By definition maxlive(Δ′) = 1, and maxlive(Δ) ≥ maxlive(Δ′) by Lemma 6.15. Therefore, maxlive(Δ) = 1 = maxlive(s).

• If s ⟶^{τ} Θ, then s R Δ implies the existence of some Δ_{Θ} such that Δ ⟶^{τ̂}^{∗} Δ_{Θ} and Θ \overline{R} Δ_{Θ}. By induction, using (ii), maxlive(Θ) ≤ maxlive(Δ_{Θ}). Consequently, we have that

maxlive(s) = max({maxlive(Θ) | s ⟶^{τ} Θ})
≤ max({maxlive(Δ_{Θ}) | s ⟶^{τ} Θ})
≤ max({maxlive(Δ) | s ⟶^{τ} Θ})  (by Lemma 6.15)
= maxlive(Δ)

(ii) Θ \overline{R} Δ means

Θ = ∑_{i∈I} p_{i} · \overline{s_{i}},  s_{i} R Δ_{i},  Δ = ∑_{i∈I} p_{i} · Δ_{i}

So we can derive that

maxlive(Θ) = ∑_{i∈I} p_{i} · maxlive(s_{i}) ≤ ∑_{i∈I} p_{i} · maxlive(Δ_{i})  (by induction) = maxlive(Δ)  □

We now have all of the ingredients to prove that showing P ⊑_{S} Q is a sound method of establishing P ⊑_{pmay} Q.

Theorem 6.17 P ⊑_{S} Q implies P ⊑_{pmay} Q.

Proof. Suppose P ⊑_{S} Q. Because of Proposition 6.14 it is sufficient to prove maxlive(⟦T |_{Act} P ⟧) ≤ maxlive(⟦T |_{Act} Q⟧) for an arbitrary test T. Since ⊑_{S} is preserved by the parallel operator we have that T |_{Act} P ⊑_{S} T |_{Act} Q. (Strictly speaking, since ω is not actually allowed to appear in processes, here we can replace it in T with a fresh action ν ∈ Act, and accordingly use |_{Act\{ν}} instead of |_{Act}.) By definition T |_{Act} P ⊑_{S} T |_{Act} Q means that there is a distribution Δ and a simulation R such that ⟦T |_{Act} Q⟧ ⟹^{τ̂} Δ and ⟦T |_{Act} P ⟧ \overline{R} Δ. The result now follows from the second part of Proposition 6.16 and Lemma 6.15. □

6.5 Some properties of simulations

Because of the co-inductive nature of the definition of simulations we can begin to develop properties of the preorder ⊑_{S} on pCSP terms. By Theorem 6.17, any equation P = Q or P ⊑ Q that we show to be sound for ≃_{S}, respectively ⊑_{S}, is also sound for ≃_{pmay}, respectively ⊑_{pmay}. In section 4 we have seen that many of the equations true for standard testing no longer apply to probabilistic processes. But some interesting identities can be salvaged.

Proposition 6.18 All the equations in Figure 8 are valid for ≃_{S} over pCSP.

Proof.

• Case (I1): It is clear that P ⊑_{S} P ⊓ P since ⟦P ⊓ P ⟧ = \overline{P ⊓ P} ⟶^{τ} ⟦P ⟧ and ⟦P ⟧ \overline{⊳_{S}} ⟦P ⟧. For the inverse direction, observe that P ⊓ P ⊳_{S} ⟦P ⟧ because the transition P ⊓ P ⟶^{τ} ⟦P ⟧ is matched by ⟦P ⟧ ⟹^{τ̂} ⟦P ⟧. Therefore we have ⟦P ⊓ P ⟧ = \overline{P ⊓ P} \overline{⊳_{S}} ⟦P ⟧, thus P ⊓ P ⊑_{S} P.

• Case (I3): Think for the moment of P ⊓ Q ⊓ R as the ternary instance of a new auxiliary operator ⨅_{i∈I} P_{i} with I a finite index set, whose operational semantics consists of the transitions ⨅_{i∈I} P_{i} ⟶^{τ} P_{i} for i ∈ I. Now we show P ⊓ Q ⊓ R ≃_{pmay} (P ⊓ Q) ⊓ R, and the proof of P ⊓ Q ⊓ R ≃_{pmay} P ⊓ (Q ⊓ R) goes likewise.

That P ⊓ Q ⊓ R ⊳_{S} (P ⊓ Q) ⊓ R follows because a move \overline{P ⊓ Q ⊓ R} ⟶^{τ} P can be simulated by a sequence of two τ-steps from \overline{(P ⊓ Q) ⊓ R}. Conversely, that

(P ⊓ Q) ⊓ R ⊳_{S} P ⊓ Q ⊓ R follows because the move \overline{(P ⊓ Q) ⊓ R} ⟶^{τ} P ⊓ Q

can be simulated by the idle τ̂-move P ⊓ Q ⊓ R ⟶^{τ̂} P ⊓ Q ⊓ R and we have P ⊓ Q ⊳_{S} P ⊓ Q ⊓ R. The latter follows because any outgoing transition of P ⊓ Q is also an outgoing transition of P ⊓ Q ⊓ R.

Given the above, and its obvious extension to the case |I| > 3, it doesn’t matter how to add brackets to the right-hand sides of (D3), (L6) and (L7); one can just GDP Festschrift ENTCS, to appear

(I1)  P ⊓ P = P
(I2)  P ⊓ Q = Q ⊓ P
(I3)  (P ⊓ Q) ⊓ R = P ⊓ (Q ⊓ R)
(P1)  P_{p}⊕ P = P
(P2)  P_{p}⊕ Q = Q_{1−p}⊕ P
(P3)  (P_{p}⊕ Q)_{q}⊕ R = P_{p·q}⊕ (Q_{\frac{(1−p)·q}{1−p·q}} ⊕ R)
(E1)  P □ 0 = P
(E2)  P □ Q = Q □ P
(E3)  (P □ Q) □ R = P □ (Q □ R)
(EI)  a.P □ b.Q = a.P ⊓ b.Q
(D1)  P □ (Q_{p}⊕ R) = (P □ Q)_{p}⊕ (P □ R)
(D2)  a.P □ (Q ⊓ R) = (a.P □ Q) ⊓ (a.P □ R)
(D3)  P □ Q = (P_{1} □ Q) ⊓ (P_{2} □ Q) ⊓ (P □ Q_{1}) ⊓ (P □ Q_{2}),
provided P = P_{1} ⊓ P_{2}, Q = Q_{1} ⊓ Q_{2}
(L1)  P |_{A} Q = Q |_{A} P
(L2)  0 |_{A} 0 = 0
(L3)  0 |_{A} a.P = \{ \begin{matrix}a.(0 |_{A} P) & if a ∉ A \\ 0 & if a ∈ A \end{matrix}
(L4)  0 |_{A} (P ⊓ Q) = (0 |_{A} P) ⊓ (0 |_{A} Q)
(L5)  a.P |_{A} b.Q = \{ \begin{matrix}0 & if a, b ∈ A and a ≠ b \\ P |_{A} Q & if a, b ∈ A and a = b \\ a.(P |_{A} b.Q) & if a ∉ A and b ∈ A \\ a.(P |_{A} b.Q) □ b.(a.P |_{A} Q) & if a, b ∉ A \end{matrix}
(L6)  (P ⊓ Q) |_{A} a.R = \{ \begin{matrix}(P |_{A} a.R) ⊓ (Q |_{A} a.R) ⊓ a.((P ⊓ Q) |_{A} R) & if a ∉ A \\ (P |_{A} a.R) ⊓ (Q |_{A} a.R) & if a ∈ A \end{matrix}
(L7)  P |_{A} Q = (P_{1} |_{A} Q) ⊓ (P_{2} |_{A} Q) ⊓ (P |_{A} Q_{1}) ⊓ (P |_{A} Q_{2})
provided P = P_{1} ⊓ P_{2}, Q = Q_{1} ⊓ Q_{2}
(L8)  P |_{A} (Q_{p}⊕ R) = (P |_{A} Q)_{p}⊕ (P |_{A} R)

Fig. 8. Some equations

as well think of these right-hand sides as instances of ⨅_{i∈I} P_{i}.

• Case (I2): It can easily be verified that ⟦P ⊓ Q⟧ \overline{⊳_{S}} ⟦Q ⊓ P ⟧ because both sides of the equation have the same outgoing transitions. Similarly for (D3), (L2–4) and (L7).

• Case (P1): By definition we have ⟦P_{p}⊕ P ⟧ = ⟦P ⟧. Similarly for (P2) and (P3).

• Case (E1): Recall that 0 is a deadlock state in S_{p}, i.e. 0 −̸→^{α} for all α ∈ Act_{τ}. Let R ⊆ S_{p} × D(S_{p}) be defined by s R Δ iff either Δ = \overline{s} or s = t □ 0 and Δ = \overline{t} for some t ∈ S_{p}. It can be checked that R is a simulation. Let ⟦P ⟧ = ∑_{j∈J} p_{j} · \overline{s_{j}}. Then ⟦P □ 0 ⟧ = ∑_{j∈J} p_{j} · \overline{s_{j} □ 0}, thus ⟦P □ 0 ⟧ \overline{R} ⟦P ⟧ and ⟦P □ 0 ⟧ \overline{⊳_{S}} ⟦P ⟧. Therefore we have P □ 0 ⊑_{S} P. Similarly we can prove P ⊑_{S} P □ 0.

• Case (E2): Let R ⊆ S_{p} × D(S_{p}) be defined by s R Δ iff either Δ = \overline{s} or s = t_{1} □ t_{2} and Δ = \overline{t_{2} □ t_{1}} for some t_{1}, t_{2} ∈ S_{p}. It can be checked that R is a simulation. Now it is easy to show that ⟦P □ Q⟧ \overline{⊳_{S}} ⟦Q □ P ⟧, thus P □ Q ⊑_{S} Q □ P. The proof of (L1) goes likewise.

• Case (E3): Let R ⊆ S_{p} × D(S_{p}) be defined by s R Δ iff either s = (t_{1} □ t_{2}) □ t_{3} and Δ = \overline{t_{1} □ (t_{2} □ t_{3})} for some t_{1}, t_{2}, t_{3} ∈ S_{p} or Δ = \overline{s}. It can be checked that R is a simulation. Again it is easy to show that ⟦(P □ Q) □ R⟧ \overline{⊳_{S}} ⟦P □ (Q □ R)⟧, hence (P □ Q) □ R ⊑_{S} P □ (Q □ R). The other direction goes likewise.

• Case (EI): Let R_{1} and R_{2} be the processes on the left and right hand side of the equation. It can be checked that both ⟦R_{1}⟧ \overline{⊳_{S}} ⟦R_{2}⟧ and ⟦R_{2}⟧ \overline{⊳_{S}} ⟦R_{1}⟧ hold. In particular, the τ-move from R_{2} to a.P can be simulated by the idle move R_{1} ⟹^{τ̂} R_{1}, since we also have ⟦a.P ⟧ \overline{⊳_{S}} ⟦R_{1}⟧. Similarly for (L6).

• Case (D1): ⟦P □ (Q_{p}⊕ R)⟧ = ⟦P ⟧ □ (p · ⟦Q⟧ + (1 − p) · ⟦R⟧) = p · (⟦P ⟧ □ ⟦Q⟧) + (1 − p) · (⟦P ⟧ □ ⟦R⟧) = ⟦(P □ Q)_{p}⊕ (P □ R)⟧. Similarly for (L8).

• Cases (D2) and (L5): It is trivial to construct simulations in both directions. □

It can be argued that the equations (L1–8) are not all that interesting, because they merely apply to our own parallel composition operator. The reason to mention them here, is that, as we will see below, they allow the parallel operator to be eliminated from pCSP expressions, and we believe the same can be achieved, with similar axioms, for the more traditional parallel composition and hiding operators of CSP.

We also have certain inequations which are valid for ⊑_{S}, the most obvious being

(May1)  P ⊑ P ⊓ Q

More inequations are listed in Figure 9. The inequations (Q1–8) complement the counterexamples 4.1–4.8. In each case, an equation that holds in non-probabilistic may-testing semantics is salvaged in the shape of an inequation, with a counterexample against the opposite direction.

Proposition 6.19 All the inequations in Figure 9 are valid for ⊑_{S} over pCSP.

Proof. The soundness of (Q0) and (Q1) is easy to check. All other inequations can be derived from (Q0), (May1) and the equations in Figure 8 by using the

(Q0)  0 ⊑ P
(Q1)  a.(P_{p}⊕ Q) ⊑ a.P_{p}⊕ a.Q
(Q2)  a.P ⊓ a.Q ⊑ a.(P ⊓ Q)
(Q3)  a.P □ a.Q ⊑ a.(P □ Q)
(Q4)  P ⊑ P □ Q
(Q5)  (P_{p}⊕ Q) ⊓ (P_{p}⊕ R) ⊑ P_{p}⊕ (Q ⊓ R)
(Q6)  P ⊓ (Q_{p}⊕ R) ⊑ (P ⊓ Q)_{p}⊕ (P ⊓ R)
(Q7)  (P □ Q) ⊓ (P □ R) ⊑ P □ (Q ⊓ R)
(Q8)  P ⊓ (Q □ R) ⊑ (P ⊓ Q) □ (P ⊓ R)

Fig. 9. Some inequations

precongruence property of ⊑_{S}. For example, we can reason

\begin{aligned}P & = P □ 0 & by (E1) \\ & ⊑ P □ Q & by (Q0) \end{aligned}

so as to obtain (Q4).

We can also reason

a.P □ a.Q ⊑ a.(P □ Q) □ a.(P □ Q)  by (Q4)
= a.(P □ Q) ⊓ a.(P □ Q)  by (EI)
= a.(P □ Q)  by (I1)

so as to obtain (Q3).

As another example, we can reason

P ⊓ (Q_{p}⊕ R) = (P_{p}⊕ P) ⊓ (Q_{p}⊕ R)  by (P1)
⊑ ((P ⊓ Q)_{p}⊕ (P ⊓ R)) ⊓ ((P ⊓ Q)_{p}⊕ (P ⊓ R))  by (May1)(4×)
= (P ⊓ Q)_{p}⊕ (P ⊓ R)  by (I1)

so as to obtain (Q6). □

Another important inequation that follows from (May1) and (P1) is

P_{p}⊕ Q ⊑ P ⊓ Q

saying that any probabilistic choice can be simulated by an internal choice.

Now with these equations and inequations, together with Theorem 6.13 we have the beginnings of an algebraic theory for pCSP processes. An application of this theory is to show that the use of the parallel composition and external choice operators can be eliminated. Let us use P =_{E} Q to indicate that P = Q can be derived using applications of the equations in Figure 8, without the inequations. Then define standard processes to be the least subset of pCSP satisfying:

(i) 0 ∈ standardP (ii) a.P ∈ standardP, whenever P ∈ standardP (iii) P_{1} ⊓ P_{2} ∈ standardP, whenever P_{i} ∈ standardP (iv) P_{1}_{p}⊕ P_{2} ∈ standardP, whenever P_{i} ∈ standardP.

Proposition 6.20 For every P in pCSP there exists a standard process sf(P) such that P =_{E} sf(P).

Proof. By induction on the structure of P. □

7 Another look at CSP

We have already seen that probabilistic tests have greater distinguishing power than purely nondeterministic tests, when applied to processes in CSP, that is those which contain no probabilistic choice. In Example 4.2 we have seen that a.(P ⊓ Q) and a.P ⊓ a.Q can be distinguished using a probabilistic test, while it is well known that they can not be distinguished using non-probabilistic tests [Hen88]. In this section we look briefly at the theory of CSP relative to probabilistic testing; we concentrate on may testing, although again similar results can be obtained for must testing.

First we have the converse of Theorem 6.17, showing that simulations are both sound and complete with respect to probabilistic may testing for this sub-language.

Theorem 7.1 For P, Q ∈ CSP, P ⊑_{pmay} Q if and only if P ⊑_{S} Q.

Proof. (⇐) This implication is proved in Theorem 6.17.

(⇒) Instead of directly showing that ⊑_{pmay} implies ⊑_{S}, we define a seemingly weaker preorder ⊑_{w}:

P ⊑_{w} Q iff for every test T: (maxlive(⟦T |_{Act} P ⟧) = 1) ⇒ (maxlive(⟦T |_{Act} Q⟧) = 1).

By Proposition 6.14, we can see that ⊑_{pmay} implies ⊑_{w}. If we can show that ⊑_{w} is a simulation, then we are done because P ⊑_{pmay} Q will imply P ⊑_{S} Q.

Given P ⊑_{w} Q and P ⟶^{α} P′, we want to find a process Q′ such that Q ⟹^{α̂} Q′ and P′ ⊑_{w} Q′. We distinguish two cases.

(i) α = τ. Then ⟦T |_{Act} P ⟧ ⟶^{τ} ⟦T |_{Act} P′⟧ for every test T, so P′ ⊑_{w} P by Lemma 6.15 and hence P′ ⊑_{w} Q. By taking Q′ = Q, we complete the proof for this case.

(ii) α = a for some a ∈ Act. We define the set Z = {R | Q ⟹^{â} R and P′ ⋢_{w} R}. As Q is a CSP process, Z is always finite. For each R ∈ Z there must be a test T_{R} such that maxlive(⟦T_{R} |_{Act} P′⟧) = 1 but maxlive(⟦T_{R} |_{Act} R⟧) < 1. Let T_{Z} be the test ⨁_{R∈Z} p_{R}T_{R}, where each p_{R} is a positive probability. Then

maxlive(⟦T_{Z} |_{Act} P′⟧) = ∑_{R∈Z} p_{R} · maxlive(⟦T_{R} |_{Act} P′⟧) = 1

and, for all R′ ∈ Z,

maxlive(⟦T_{Z} |_{Act} R′⟧) = ∑_{R∈Z} p_{R} · maxlive(⟦T_{R} |_{Act} R′⟧) < 1

So we have maxlive(⟦a.T_{Z} |_{Act} P ⟧)=1, which implies maxlive(⟦a.T_{Z} |_{Act} Q⟧)=1 since P ⊑_{w} Q. By the definition of maxlive( ) there exists a Q′ such that Q ⟶^{τ}^{∗}⟶^{a} Q′ and maxlive(⟦T_{Z} |_{Act} Q′⟧)=1. Thus Q′ ∉ Z, and P′ ⊑_{w} Q′. □

We can also give a complete equational characterisation. The extra axiom which is valid for this non-probabilistic sub-language is

(May2)  P □ Q = P ⊓ Q

In particular this means that, as with standard testing, there is no difference between internal and external choice. Now let us write P ⊑_{E_{may}} Q to denote the fact that P ⊑ Q can be derived using the equations of Figure 8 and the inequations (May1) and (May2).

Theorem 7.2 For P, Q ∈ CSP, P ⊑_{pmay} Q if and only if P ⊑_{E_{may}} Q.

Proof. One direction follows from the fact that all the equations and inequations mentioned are valid for ⊑_{S}. The converse depends on being able to rewrite all processes into a normal form: □_{i∈I} a_{i}.P_{i}, where I is a finite and possibly empty index set, is a normal form if each P_{i} is in turn a normal form. This conversion into normal form is enabled by Proposition 6.20 and (May2). Using (May1), (E1–3) and the law P □ P = P, which follows from (May2) and (I1), it is straightforward to show that for normal forms

□_{i∈I} a_{i}.P_{i} ⊑_{S} □_{j∈J} b_{j}.Q_{j} implies □_{i∈I} a_{i}.P_{i} ⊑_{E_{may}} □_{j∈J} b_{j}.Q_{j} □

8 Related work

Models for probabilistic concurrent systems have been studied for a long time [Rab63,Der70,Var85,JP89]. One of the first models obtained as a simple adaptation of the traditional labelled transition systems from concurrency theory appears in [LS91]. Their probabilistic transition systems are classical labelled transition systems, where in addition every transition is labelled with a probability, a real number in the interval [0,1], such that for every state s and every action a, the probabilities of all a-labelled transitions leaving s sum up to either 0 or 1.

In [GJS90] a similar model was proposed, but where the probabilities of all transitions leaving s sum up to either 0 or 1. [GSST90] propose the terminology reactive for the type of model studied in [LS91], and generative for the type of model studied in [GJS90]. In a generative model, a process can be considered to spontaneously generate actions, unless restricted by the environment; in generating actions, a probabilistic choice is made between all transitions that can be taken from a given state, even if they have different labels. In a reactive model, on the other hand, processes are supposed to perform actions only in response to requests by the environment. The choice between two different actions is therefore not under the control of the process itself. When the environment requests a specific action, a probabilistic choice is made between all transitions (if any) that are labelled with the requested action.

In the above-mentioned models, the nondeterministic choice that can be modelled by non-probabilistic labelled transition systems is replaced by a probabilistic choice (and in the generative model also a deterministic choice, a choice between different actions, is made probabilistic). Hence reactive and generative probabilistic transition systems do not generalise non-probabilistic labelled transition systems. A model, or rather a calculus, that features both nondeterministic and reactive probabilistic choice was proposed in [HJ90]. It was slightly reformulated in [SL94] under the name simple probabilistic automata, and is essentially the same model we use in this paper.

Following the classification above, our model is reactive rather than generative. The reactive model of [LS91] can be reformulated by saying that a state s has at most one outgoing transition for any action a, and this transition ends in a probability distribution over its successor states. The generalisation of [SL94], that we use here as well, is that a state can have multiple outgoing transitions with the same label, each ending in a probability distribution. Simple probabilistic automata are a special case of the probabilistic automata of [SL94], that also generalise the generative models of probabilistic processes to a setting with nondeterministic choice.

8.1 Bisimulation, and the alternating approach

Whereas the testing semantics explored in the present paper is based on the idea that processes should be distinguished only when there is a compelling reason to do so, (strong) bisimulation semantics [Mil89] is based on the idea that processes should be identified only when there is a compelling reason to do so. It has been extended to reactive probabilistic processes in [LS91], to generative ones in [GSST90], and to processes combining nondeterminism and probability in [HJ90]. The latter paper also features a complete axiomatisation of a probabilistic extension of recursion-free CCS.

Weak and branching bisimulation [Mil89,GW96] are versions of strong bisimulation that respect the hidden nature of the internal action τ. Generalisations of these notions to nondeterministic probabilistic processes appear, amongst others, in [SL94,Seg95,PLS00,AB01,BS01,DP05,AW06], with complete axiomatisations reported in [BS01,DP05,DPP05,ABW06]. The authors of these paper tend to distinguish whether they work in an alternating [PLS00,AB01,AW06,ABW06] or a non-alternating model of probabilistic processes [SL94,Seg95,DP05,DPP05], the two approaches being compared in [BS01]. The non-alternating model stems from [SL94] and is similar to our model of Section 3.2. The alternating model is attributed to [HJ90], and resembles our graphical representation of processes in Section 3.4. It is easy to see that mathematically the alternating and non-alternating model can be translated into each other without loss of information [BS01]. The difference between the two is one of interpretation. In the alternating interpretation, the nodes of form ∘ in our graphical representations are interpreted as actual states a process can be in, whereas in the non-alternating representation they are not. Take for example the process R_{1} = a.(b _{\frac{1}{2}} ⊕ c) depicted in Figure 5. In the alternating representation this process passes through a state in which a has already happened, but the probabilistic choice between b and c has not yet been made. In the non-alternating interpretation on the other hand the execution of a is what constitutes this probabilistic choice; after doing a there is a fifty-fifty change of ending up in either state. Although in strong bisimulation semantics the alternating and non-alternating interpretation lead to the same semantic equivalence, in weak and branching bisimulation semantics the resulting equivalences are different, as illustrated in [PLS00,BS01,AW06]. Our testing and simulation preorders as presented here can be classified as non-alternating; however, we believe that an alternating approach would lead to the very same preorders.

8.2 Testing

Generalisations of the testing theory of [DH84] to probabilistic systems first appear in [Chr90] and [CSZ92], for generative processes without nondeterministic choice. The application of testing to the probabilistic processes we consider here stems from [WL92]. In [Seg96] a richer testing framework is proposed, for essentially the same class of processes, namely one in which multiple success actions ω_{i} for i = 1, 2, … exists, and the application of a test to a process yields not a set of real numbers, indicating success probabilities, but a set of tuples of real numbers, the i^{th} component in the tuple indicating the success probability of ω_{i}.

In [JHW94], a testing theory is proposed that associates a reward, a non-negative real number, to every success-state in a test process; in calculating the set of results of applying a test to a process, the probabilities of reaching a success-state are multiplied by the reward associated to that state. They allow non-probabilistic tests only, but apply these to arbitrary nondeterministic probabilistic processes, and provide a trace-like denotational characterisation of the resulting may-testing preorder. Denotational characterisations of the variant of our testing preorders in which only τ-free processes are allowed as test-processes appear in [JW95,JW99]. These characterisations are improved in [JW02], discussed below.

In [CCR^{+}03] a testing theory for nondeterministic probabilistic processes is developed in which, as in [MMSS96], all probabilistic choices are resolved first. A consequence of this is that the idempotence of internal choice (our axiom (I1)) must be sacrificed. Some papers distill preorders for probabilistic processes by means of testing scenarios in which the premise that a test is itself a process is given up. These include [LS91,KN98] and [SV03].

8.3 Simulations

Four different notions of simulation for probabilistic processes occur in the literature, each a generalisation of the well know concept of simulation for nondeterministic processes [Par81]. The most straightforward generalisation [JL91] defines a simulation as a relation R between states, satisfying, for all s, t, α, Θ,

if s R t and s ⟶^{α} Θ then there is a Δ′ with t ⟶^{α} Δ′ and Θ \overline{R} Δ′.

This simulation induces a preorder that does not satisfy the law

a.(P_{p}⊕ Q) ⊑ a.P □ a.Q

which holds in probabilistic may testing semantics. The reason is that the process a.P □ a.Q can answer the initial a-move of a.(P _{p}⊕ Q) by taking either the amove to P, or the a-move to Q, but not by a probabilistic combination of the two. Such probabilistic combinations are allowed in the probabilistic simulation of [SL94], which induces a coarser preorder on processes, satisfying the above law. In our terminology it can be defined by changing the requirement above into

if s R t and s ⟶^{α} Θ then there is a Δ′ with \overline{t} ⟶^{α} Δ′ and Θ \overline{R} Δ′.

A weak version of this probabilistic simulation, abstracting from the internal action τ, weakens this requirement into

if s R t and s ⟶^{α} Θ then there is a Δ′ with \overline{t} ⟹^{α̂} Δ′ and Θ \overline{R} Δ′.

Nevertheless, also this probabilistic simulation does not satisfy all the laws we have shown to hold for probabilistic may testing. In particular, it does not satisfy the

law a.(P_{p}⊕ Q) ⊑ a.P_{p}⊕ a.Q.

Consider for instance the processes R_{1} = a.b.c.(d_{\frac{1}{2}} ⊕ e) and R_{2} = a.(b.c.d_{\frac{1}{2}} ⊕ b.c.e). The law (Q1) above, which holds for probabilistic may testing, would yield R_{1} ⊑ R_{2}. If we are to relate these processes via a probabilistic simulation à la [SL94], the state c.(d_{\frac{1}{2}} ⊕ e) of R_{1}, reachable after an a and a b-step, needs to be related to the distribution (c.d_{\frac{1}{2}} ⊕ c.e) of R_{2}, containing the two states a.b and a.c. This relation cannot be obtained through lifting, as this would entail relating the single state c.(d _{\frac{1}{2}} ⊕ e) to each of the states c.d and c.e. Such a relation would not be sound, because c.(d _{\frac{1}{2}} ⊕ e) is able to perform the sequence of actions ce half of the time, whereas the process c.d cannot mimic this.

In [JW02], another notion of simulation is proposed, whose definition is too complicated to explain in a few sentences. They show for a class of probabilistic processes that do not contain τ-actions, that probabilistic may testing is captured exactly by their notion of simulation. Nevertheless, their notion of simulation makes strictly more identifications than ours. As an example, consider the processes R_{1} = a _{\frac{1}{2}} ⊕ (b □ c) and R_{3} = (a □ b) _{\frac{1}{2}} ⊕ (a □ c) of Example 4.9, which also appear in Section 5 of [JW02]. There it is shown that R_{1} ⊑ R_{3} holds in their semantics. However, in our framework we have R_{1} ⋢_{pmay} R_{3}, as demonstrated in Example 4.9. The difference can only be explained by the circumstance that in [JW02] processes, and hence also tests, may not have internal actions. So this example shows that tests with internal moves can distinguish more processes than tests without internal moves, even when applied to processes that have no internal moves themselves.

Our notion of simulation first appears in [Seg95], although the preorder ⊑_{S} of Definition 6.3 is new. Segala has no expressions that denote distributions and consequently is only interested in the restriction of the simulation preorder to states (automata in his framework). It turns out that for states s and t (which in our framework are expressions in the set S_{p}) we have s ⊑_{S} t iff s ⊳_{S} \overline{t}, so on their common domain of definition, the simulation preorder of [Seg95] agrees with ours.

This notion of simulation is strictly more discriminating than the simulation of [JW02], and strictly less discriminating than the ones from [SL94] and [JL91]. We conjecture that, for the class of processes considered in this paper, it captures probabilistic may testing exactly, i.e. that P ⊑_{S} Q iff P ⊑_{pmay} Q. In [LSV03] it has been shown that the simulation preorder of [Seg95] coincides with the congruence closure of inclusion of sets of trace distributions, a preorder also defined in [Seg95]. In [Seg96] it has been shown that the latter notion coincides with the preorder generated by Segala’s different form of probabilistic may testing, mentioned earlier, in which there are countably many different success actions, and the set of outcomes O consists of the countably-dimensional vectors over the unit interval [0,1]. To the best of our knowledge, the question whether this form of testing yields the same preorders as the notion of testing from [WL92] and our paper is, as of yet, unanswered.

References

[AB01] S. Andova & J.C.M. Baeten (2001): Abstraction in probabilistic process algebra. In Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, LNCS 2031, Springer, pp. 204–219.

[ABW06] S. Andova, J.C.M. Baeten & T.A.C. Willemse (2006): A complete axiomatisation of branching bisimulation for probabilistic systems with an application in protocol verification. In Proceedings of the 17th International Conference on Concurrency Theory, LNCS 4137, Springer, pp. 327–342.

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

[AW06] S. Andova & T.A.C. Willemse (2006): Branching bisimulation for probabilistic systems: Characteristics and decidability. Theoretical Computer Science 356(3), pp. 325–355.

[BHR84] S.D. Brookes, C.A.R. Hoare & A.W. Roscoe (1984): A theory of communicating sequential processes. Journal of the ACM 31(3), pp. 560–599.

[BJ78] D. Bjørner & C.B. Jones, editors (1978): The Vienna Development Method: The Meta-Language, LNCS 61. Springer.

[BS01] E. Bandini & R. Segala (2001): Axiomatizations for probabilistic bisimulation. In Proceedings of the 28th International Colloquium on Automata, Languages and Programming, LNCS 2076, Springer, pp. 370–381.

[CCR^{+}03] D. Cazorla, F. Cuartero, V.V. Ruiz, F.L. Pelayo & J.J. Pardo (2003): Algebraic theory of probabilistic and nondeterministic processes. Journal of Logic and Algebraic Programming 55(1-2), pp. 57–103.

[Chr90] I. Christoff (1990): Testing equivalences and fully abstract models for probabilistic processes. In Proceedings the 3rd International Conference on Concurrency Theory, LNCS 458, Springer, pp. 126–140.

[CSZ92] R. Cleaveland, S.A. Smolka & A.E. Zwarico (1992): Testing preorders for probabilistic processes. In Proceedings of the 19th International Colloquium on Automata, Languages and Programming, LNCS 623, Springer, pp. 708–719.

[Der70] C. Derman (1970): Finite State Markovian Decision Processes. Academic Press.

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

[DP05] Y. Deng & C. Palamidessi (2005): Axiomatizations for probabilistic finite-state behaviors. In Proceedings of the 8th International Conference on Foundations of Software Science and Computation Structures, LNCS 3441, Springer, pp. 110–124.

[DPP05] Y. Deng, C. Palamidessi & J. Pang (2005): Compositional reasoning for probabilistic finite-state behaviors. In Processes, Terms and Cycles: Steps on the Road to Infinity, Essays Dedicated to Jan Willem Klop, on the Occasion of His 60th Birthday, LNCS 3838, Springer, pp. 309–337.

[ER64] C.C. Elgot & A. Robinson (1964): Random-access stored-program machines, an approach to programming languages. Journal of the ACM 11(4), pp. 365–399.

[GJS90] A. Giacalone, C.-C. Jou & S.A. Smolka (1990): Algebraic reasoning for probabilistic concurrent systems. In Proceedings of IFIP TC 2 Working Conference on Programming Concepts and Methods, pp. 443–458.

[GSST90] R.J. van Glabbeek, S.A. Smolka, B. Steffen & C.M.N. Tofts (1990): Reactive, generative, and stratified models of probabilistic processes. In Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science, Computer Society Press, pp. 130–141.

[GW96] R.J. van Glabbeek & W.P. Weijland (1996): Branching time and abstraction in bisimulation semantics. Journal of the ACM 43(3), pp. 555–600.

[Hen82] M. Hennessy (1982): Powerdomains and nondeterministic recursive definitions. In Proceedings of the 5th International Symposium on Programming, LNCS 137, Springer, pp. 178–193.

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

[HJ90] H. Hansson & B. Jonsson (1990): A calculus for communicating systems with time and probabilities. In Proceedings of the Real-Time Systems Symposium (RTSS ’90), Computer Society Press, pp. 278–287.

[Hoa85] C.A.R. Hoare (1985): Communicating Sequential Processes. Prentice-Hall.

[HSM97] Jifeng He, K. Seidel & A.K. McIver (1997): Probabilistic models for the guarded command language. Science of Computer Programming 28, pp. 171–192.

[JHW94] B. Jonsson, C. Ho-Stuart & Wang 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.

[JL91] B. Jonsson & K.G. Larsen (1991): Specification and refinement of probabilistic processes. In Proceedings of the 6th Annual IEEE Symposium on Logic in Computer Science, Computer Society Press, pp. 266–277.

[JP89] C. Jones & G. Plotkin (1989): A probabilistic powerdomain of evaluations. In Proceedings of the 4th Annual IEEE Symposium on Logic in Computer Science, Computer Society Press, pp. 186–195.

[JW95] B. Jonsson & Wang Yi (1995): Compositional testing preorders for probabilistic processes. In Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science, Computer Society Press, pp. 431–441.

[JW99] B. Jonsson & Wang Yi (1999): Fully abstract characterization of probabilistic may testing. In Proceedings of the 5th International AMAST Workshop on Formal Methods for Real-Time and Probabilistic Systems, LNCS 1601, Springer, pp. 1–18.

[JW02] B. Jonsson & Wang Yi (2002): Testing preorders for probabilistic processes can be characterized by simulations. Theoretical Computer Science 282(1), pp. 33–51.

[JWL01] B. Jonsson, Wang Yi & K.G. Larsen (2001): Probabilistic extensions of process algebras. In Handbook of Process Algebra, chapter 11, Elsevier, pp. 685–710.

[KN98] M.Z. Kwiatkowska & G. Norman (1998): A testing equivalence for reactive probabilistic processes. Electronic Notes in Theoretical Computer Science, 16(2).

[Lan63] P.J. Landin (1963): The mechanical evaluation of expressions. Computer Journal 6(4), pp. 308–320.

[Low93] G. Lowe (1993): Representing nondeterminism and probabilistic behaviour in reactive processes. Technical Report TR-11-93, Computing laboratory, Oxford University.

[Low95] G. Lowe (1995): Probabilistic and prioritized models of timed CSP. Theoretical Computer Science 138, pp. 315–352.

[LS91] K.G. Larsen & A. Skou (1991): Bisimulation through probabilistic testing. Information and Computation 94(1), pp. 1–28.

[LS92] K.G. Larsen & A. Skou (1992): Compositional verification of probabilistic processes. In Proceedings of the 3rd International Conference on Concurrency Theory, LNCS 630, Springer, pp. 456–471.

[LSV03] N. Lynch, R. Segala & F.W. Vaandrager (2003): Compositionality for probabilistic automata. In Proceedings of the 14th International Conference on Concurrency Theory, LNCS 2761, Springer, pp. 204–222.

[Luc71] P. Lucas (1971): Formal definition of programming languages and systems. In IFIP Congress, volume 1, pp. 291–297.

[Mil89] R. Milner (1989): Communication and Concurrency. Prentice-Hall.

[Mis00] M.W. Mislove (2000): Nondeterminism and probabilistic choice: Obeying the laws. In Proc. of CONCUR’00, LNCS 1877, Springer, pp. 350–364.

[MM01] A.K. McIver & C.C. Morgan (2001): Partial correctness for probabilistic programs. Theoretical Computer Science 266(1–2), pp. 513–41.

[MMS96] C.C. Morgan, A.K. McIver & K. Seidel (1996): Probabilistic predicate transformers. ACM Transactions on Programming Languages and Systems 18(3), pp. 325–353.

[MMSS96] C.C. Morgan, A.K. McIver, K. Seidel & J.W. Sanders (1996): Refinement-oriented probability for CSP. Formal Aspects of Computing 8(6), pp. 617–47.

[MOW04] M.W. Mislove, J. Ouaknine & J. Worrell (2004): Axioms for probability and nondeterminism. Electronic Notes in Theoretical Computer Science 96, pp. 7–28.

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

[Par81] D.M.R. Park (1981): Concurrency and automata on infinite sequences. In Proceedings of 5th GI Conference, LNCS 104, Springer, pp. 167–183.

[Plo81] G.D. Plotkin (1981): A Structural Approach to Operational Semantics. Technical Report DAIMI FN-19, University of Aarhus.

[Plo04] G.D. Plotkin (2004): A Structural Approach to Operational Semantics. Journal of Logic and Algebraic Programming 60-61, pp. 17–139.

[PLS00] A. Philippou, I. Lee & O. Sokolsky (2000): Weak bisimulation for probabilistic systems. In Proceedings of the 11th International Conference on Concurrency Theory, LNCS 1877, Springer, pp. 334–349.

[Rab63] M.O. Rabin (1963): Probabilistic automata. Information and Control 6, pp. 230–245.

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

[Seg96] R. Segala (1996): Testing probabilistic automata. In Proceedings of the 7th International Conference on Concurrency Theory, LNCS 1119, Springer, pp. 299–314.

[SL94] R. Segala & N.A. Lynch (1994): Probabilistic simulations for probabilistic processes. In Proceedings of the 5th International Conference on Concurrency Theory, LNCS 836, Springer, pp. 481–496.

[SV03] M.I.A. Stoelinga & F.W. Vaandrager (2003): A testing scenario for probabilistic automata. In Proceedings of the 30th International Colloquium on Automata, Languages and Programming, LNCS 2719, Springer, pp. 407–18.

[TKP05] R. Tix, K. Keimel & G.D. Plotkin (2005): Semantic domains for combining probability and non-determinism. Electronic Notes in Theoretical Computer Science 129, pp. 1–104.

[Var85] M.Y. Vardi (1985): Automatic verification of probabilistic concurrent finite-state programs. In Proceedings 26th Annual Symposium on Foundations of Computer Science, pp. 327–338.

[VW06] D. Varacca & G. Winskel (2006): Distributing probability over non-determinism. Mathematical Structures in Computer Science 16(1), pp. 87–113.

[WL92] Wang Yi & K.G. Larsen (1992): Testing probabilistic and nondeterministic processes. In Proceedings of the IFIP TC6/WG6.1 Twelfth International Symposium on Protocol Specification, Testing and Verification, IFIP Transactions C-8, North-Holland, pp. 47– 61.