9512.net
ÌðÃÎÎÄ¿â
µ±Ç°Î»ÖÃ£ºÊ×Ò³ >> >>

Reactive, generative, and stratified models of probabilistic processes

Reactive, Generative and Strati ed Models of Probabilistic Processes
Computer Science Department, Stanford University Stanford, CA 94305-2140, USA
rvg@cs.stanford.edu

Rob J. van Glabbeek

Department of Computer Science, SUNY at Stony Brook Stony Brook, NY 11794-4400, USA
sas@cs.sunysb.edu

Scott A. Smolkay

Institut fur Mathematik und Informatik, Universitat Passau 94040 Passau, Germany
bus@fmi.uni-passau.de

Bernhard Ste en

We introduce three models of probabilistic processes, namely, reactive, generative and strati ed. These models are investigated within the context of PCCS, an extension of Milner's SCCS in which each summand of a process summation expression is guarded by a probability and the sum of these probabilities is 1. For each model we present a structural operational semantics of PCCS and a notion of bisimulation equivalence which we prove to be a congruence. We also show that the models form a hierarchy: the reactive model is derivable from the generative model by abstraction from the relative probabilities of di erent actions, and the generative model is derivable from the strati ed model by abstraction from the purely probabilistic branching structure. Moreover the classical nonprobabilistic model is derivable from each of these models by abstraction from all probabilities.

1 Introduction
In the reactive model Pnu85] of classical concurrency theory, a process reacts to stimuli presented by its environment. A mechanistic view of the reactive model has been given by Milner Mil80] in terms of button pushing experiments. The environment or observer experiments on a process by attempting to depress one of several buttons that the process possesses as its interface to the outside world. The experiment succeeds if the button is unlocked and therefore goes down; otherwise
Research supported in part by ONR Grant N00014-92-J-1974. Research supported in part by NSF Grants CCR-8704309, CCR{9120995, and CCR{9208585; and AFOSR Grant F49620-93-1-0250.
y

1

a
d

1 4

HHH ] 3] Hb 1] d a4 HH d a 1] ?? @@b 1] c 1] @ ?
d d d d

P

a 1] 6
d

1 a ] ?? @@ b 2 ] ? @d d 1 2 d

Q dH HHHb 1 ] 1 a 2] H3

Hd
d

c 1]

Figure 1: Reactive process P and generative process Q. the experiment fails. In response to a successful experiment, the process makes an internal state transition and is then ready for further experimentation. The reactive model has been adopted by Larsen and Skou LS91] for probabilistic processes : a button-pressing experiment succeeds, with probability 1, or else fails. If successful, the process makes an internal state transition according to a probability distribution associated with the depressed button and the current state of the process. In the probabilistic case, it is interesting to consider a more \probabilistic" form of experimentation we call the generative model. In this setting, an observer may attempt to depress more than one button at a time. Now the process is more or less on equal footing with its environment, and will decide, according to a prescribed probability distribution, which button if any will go down. In response to a successful outcome, this same probability distribution, conditioned by the process's choice of button, will govern the internal state transition made by the process. For example, consider the reactive process P and the generative process Q given by: 1 3 1 1 P = 4 a + 4 a : (a + b) + b : c Q = 1 a + 2 a : ( 1 a + 1 b) + 3 b : c 6 2 2 P and Q have as semantics the probabilistic labeled transition systems depicted in Figure 1. For P , an a- or b-experiment will succeed with probability 1, whereas a c-experiment will fail. In the case 1 3 of an a-experiment, P will branch left with probability 4 and right with probability 4 . Note that no information is given about the relative probability of performing an a-action versus a b-action in P 's initial state. For the generative process Q, if the observer simultaneously attempts to depress the a and b 2 1 buttons, Q will unlock its a-button with probability 3 and its b-button with probability 3 . In the 3 1 former case, Q will branch left with probability 4 and right with probability 4 , which is precisely P 's reaction to an a-experiment. In fact, for any single-button experiment, P and Q behave the same. Thus Q contains strictly more information than P , and, in a broader sense, the reactive model is an abstraction of the generative model. In this paper we also consider the strati ed model of probabilistic processes, which captures the branching structure of the purely probabilistic choices made by a process. For example, consider an operating system in which there are n processes to be multiprogrammed. One of these is the garbage collector which performs optimally if given one third of the CPU cycles. The other n ? 1 processes are user processes and should equally share the remaining two thirds of the CPU. For the case n = 3, a plausible speci cation of a scheduler for these processes would be 1 1 Sc = xX ( 3 a:X + 1 b:X + 3 c:X ) 3 2

1 3

c

a %% %%Xee

c

aaaa2 3 aa c 1 1 2 " Q 2 c " " " QQ c
b

%% %%Xee

%% e %%X e

c

%% %%Xee

1 a 3]

PPPPc 1 ] 3 PPP b ] %% %% %%Xee %%Xee
c 1 3

Figure 2: Strati ed and generative transition systems of Sc0. where the action a identi es the garbage collector, and b and c the user processes. But consider the restriction context in which user c is denied further access to the machine. What would happen to its share of the CPU? Because of the symmetry in the above speci cation, we would naturally arrive at the expression 1 xX ( 2 a:X + 1 b:X ) 2 Now, however, the garbage collector is granted one half of the CPU which is di erent from our original intent. An exact speci cation of the scheduler can be obtained through the use of nested expressions of probabilistic choice: 1 Sc0 = xX ( 3 a:X + 2 ( 1 b:X + 1 c:X )) 3 2 2 which, in the strati ed model, yields the leftmost probabilistic labeled transition system of Figure 2. If user c were now denied access we would obtain 1 xX ( 3 a:X + 2 b:X ) 3 as desired. Thus, in the strati ed model, the intended relative frequencies are preserved in a level-wise fashion in the presence of restriction. Note that the probabilistic labeled transition system of Sc0 in the generative model is simply the right one of Figure 2. Thus, in the generative model, Sc is (unfortunately) equivalent to Sc0. We shall see that, in a broader sense, the generative model is an abstraction of the strati ed model, in which the branching structure of probabilistic choices has been \ attened." The extremal case of nested probabilistic choice in the strati ed model, in which zero probabilities are permitted, yields a general notion of process priority. For example, the expression 1P + 0(1Q + 0R) gives priority to process P over Q and R, and priority to Q over R. Thus process R can only be executed in a restriction context that excludes P and Q. Zero probabilities are not considered in this paper, but their role in modeling priority is examined carefully in SS90].

Summary of Technical Results
We will be working within the framework of PCCS, a speci cation language for probabilistic processes introduced in GJS90]. PCCS is derived from Milner's SCCS Mil83] by replacing the operator of nondeterministic process summation with a probabilistic counterpart. Several PCCS expressions have appeared above, which should give the avor of the language. 3

For each of the three probabilistic models, and, for comparison purposes, the classical nonprobabilistic model, we present the following: a structural operational semantics of PCCS, given as a set of inference rules in the style of Plotkin Plo81] and Milner Mil89]. For each model, these inference rules determine a semantic mapping from the set of PCCS expressions to a particular domain of probabilistic labeled transition systems. We denote these mappings as 'N , 'R , 'G , and 'S , respectively. (As discussed in Section 4, the relabeling operator of PCCS is not compatible with the reactive model, and also the combination of summation and unguarded recursion may be problematic. Therefore, 'R applies only to a sublanguage PCCSR of PCCS in which relabeling and unguarded recursion are excluded.) a notion of bisimulation semantics. In LS91], Larsen and Skou introduced probabilistic bisimulation, a natural and elegant extension of strong bisimulation Par81, Mil83] for reactive processes. We likewise de ne probabilistic bisimulation on generative and strati ed processes. In each model, the largest bisimulation (under set inclusion), denoted N , R , G , and S , respectively, determines the model's bisimulation semantics. We prove that R is a congruence with respect to PCCSR , and N , G and S are congruences with respect to PCCS. We then inter-relate the models, ultimately showing that they form a hierarchy: the generative model is an abstraction of the strati ed model, the reactive model is an abstraction of the generative model, and the nonprobabilistic model is an abstraction of the reactive model. This re ects the stepwise reduction of \observational power"; i.e. starting from the strati ed model, we rst abstract from the probabilistic branching structure, then from the relative probabilities among di erent actions, and nally from all probabilities. We proceed as follows: We add to the strati ed, generative and reactive operational semantics inter-model abstraction rules, which respectively allow the inference of generative probabilistic transitions from strati ed ones, reactive probabilistic transitions from generative ones, and nonprobabilistic transitions from reactive ones. These rules determine mappings between domains of probabilistic labeled transition systems, which are denoted as 'SG , 'GR and 'RN , respectively. Similarly we de ne \shortcuts" 'SR , 'GN and 'SN , and establish 'GN 'SG = 'RN 'SR = 'SN , 'RN 'GR = 'GN and 'GR 'SG = 'SR. The last result however only holds for strati ed transition systems speci ed by closed PCCS expressions in which each summation is probability- and action-guarded. We refer to such expressions as summation-guarded PCCS expressions. We obtain the following inter-model abstraction results . For any two strati ed transition systems G and H : G S H =) 'SG (G) G 'SG (H ) For any two generative transition systems G and H : G G H =) 'GR (G) R 'GR (H ) For any two reactive transition systems G and H : G R H =) 'RN (G) N 'RN (H ) For any two strati ed transition systems G and H : G S H =) 'SR (G) R 'SR (H ) Note that our last abstraction result holds for all strati ed transition systems and is therefore not directly obtainable from the rst two via the 'SR shortcut (which applies only to summation-guarded strati ed transition systems). 4

'N
Nonprobabilistic Model

)

'RN

Reactive Model

P ? @ PPPP ? P 'S ?'R @@ 'G PPPPP @@ PPPP ?? ' P R @ ? q P '
GR

PCCS

Generative Model

SG

Strati ed Model

Nonprobabilistic (= Bisimulation

?

Reactive Bisimulation

?

(=

Generative Bisimulation

?

(=

Strati ed Bisimulation

?

Figure 3: Interdependencies between the models. For P a closed PCCS expression we prove the following commutativity results , which, in addition to the abstraction results, establish the hierarchy among the models.

'G(P ) 'R(P ) 'R(P ) 'N (P ) 'N (P )

= = = = =

'SG ('S (P )) 'GR('G(P )) 'SR('S (P )) 'RN ('R(P )) 'SN ('S (P ))

if P is summation-guarded or restriction-free if P is a summation-guarded PCCSR expression if P is a PCCSR expression if P is a PCCSR expression = 'GN ('G (P ))

In the presence of restriction and general summation the rst commutativity result does not hold. This is to be expected, as the strati ed model is motivated by its di erent treatment of restriction with respect to nested summations. Additionally, we show that the second commutativity result does not hold in the presence of general summation. In fact, our counterexample suggests that the reactive summation has a strati ed avor that is not present in the generative case. This impression is supported by the third commutativity result, that holds without restrictions on summation or restriction. It is not possible to de ne in a compositional way a more generatively avored summation in the reactive model, that would allow a generalization of the second commutativity result. We then show that the equivalence induced on the strati ed (generative) model via abstraction to the generative (reactive) model is not a congruence with respect to PCCS. This demonstrates the need for re ning the bisimulation semantics when moving to a less abstract model. More precisely, we exhibit a pair of PCCS processes P , Q and a context C ] such that

'SG ('S (P )) G 'SG('S (Q)) and 'SG ('S (C P ])) 6 G 'SG ('S (C Q]))
Similarly for the generative-to-reactive and strati ed-to-reactive abstractions. On the other hand, the equivalence induced on the strati ed model via abstraction to the reactive model is a congruence with respect to PCCSR . Likewise, the equivalences induced on the strati ed and generative models via abstraction to the nonprobabilistic model are 5

congruences with respect to PCCS; and the equivalence induced on the reactive model via abstraction to the nonprobabilistic model is a congruence with respect to PCCSR . These congruence results can be seen as consequences of the fact that the corresponding commutativity results hold without side conditions, and that R , G , and S are congruences. The interdependencies between the di erent models are summarized in Figure 3. Here the upper part re ects the commutativity results, the double arrows below re ect the abstraction results, and the dashed arrows indicate the bisimulations that are induced on the strati ed, generative, and reactive models via abstraction to the generative, reactive, and nonprobabilistic models, respectively. We conclude the paper with an interesting open problem concerning an equivalence relation M (mixed bisimulation) that, in terms of its distinguishing strength, falls strictly between G and S , and is still a congruence in the strati ed model. We conjecture that M is the largest congruence contained in G .

Related Work
This paper is an extended version of vGSST90], which was written in cooperation with Chris Tofts. The main contributions of the current paper and vGSST90] are: { The reactive operational semantics of summation-guarded PCCSR was rst given in vGSST90]. The reactive semantics of general summation, not present in vGSST90], was developed in LS92]. The generative operational semantics of PCCS stems from GJS90]. { The strati ed model and its operational and bisimulation semantics rst appeared in vGSST90]. { All congruence results and the interrelations between the various models were indicated, in part, in vGSST90]. Their detailed proofs are given here for the rst time. Pointers to earlier, mostly logic-oriented approaches to probabilistic processes (e.g. probabilistic temporal and dynamic logic) can be found in GJS90]. Recent work on probabilistic process algebra includes LS92] (in a reactive setting), JS90, JL91, BBS92] (in a generative setting) and SS90, Tof90b] (in a strati ed setting). All these papers consider probabilistic bisimulation, except for JS90], where also probabilistic versions of trace, failure and readiness equivalences and congruences are studied. The interplay between time and probability has been investigated in HJ90, Low91]. Larsen and Skou LS91] have examined the reactive model in the setting of testing. They exhibit a testing algorithm that, with probability 1 ? , where is arbitrarily small, can distinguish processes that are not probabilistically bisimilar. Bloom and Meyer BM89] further show that if nondeterministic bounded-branching processes P and Q are bisimilar, then there is an assignment of probabilities to the edges of P and Q, yielding reactive processes P 0 and Q0 such that P 0 and Q0 are probabilistically bisimilar. Christo Chr90] also considers the testing of probabilistic processes. He proposes three probabilistic trace-based testing equivalences for generative processes using nondeterministic tests. Cleaveland et al. CSZ92] investigate the testing of generative processes as well (but with generative tests); close connections to the classical testing theory of De Nicola and Hennessy are demonstrated. 6

Similar connections are made by Yi and Larsen in YL92] for a model of probabilistic processes based on HJ90]. Jones and Plotkin JP89] investigate a probabilistic powerdomain of evaluations, which they use to give the semantics of a language with a probabilistic parallel construct. Finally, Seidel Sei92] uses conditional probability measures to give a semantics to a probabilistic extension of CSP.

2 Syntax of PCCS
As in SCCS, the atomic actions of PCCS form a multiplicative structure (Act; ) that is generated freely from the set of particulate actions. Unlike SCCS, where Act is an abelian monoid, we assume neither commutativity nor associativity for action product ( ). Thus all elements of Act are of the form a or ( ; ), where a 2 and ; 2 Act. One can think of the atomic action ( ; ) as the simultaneous ordered occurrence of actions and . As discussed in Section 4, the free structure of our action algebra is necessary to be able to de ne synchronous product in the reactive model. For any SCCS-like action monoid or group, the corresponding synchronization merge can be expressed in our calculus by a combination of product and relabeling. For example, the group structure of SCCS can be obtained through relabelings of the form ( ; ) 7! 1 and ( ; ) 7! 1 , where 1 is the unit or idle action of SCCS. As a consequence relabeling, which is a derived operator in SCCS in the sense that it can be expressed in terms of the other operators, has to be introduced as a rst-class operator in PCCS. Let X be a variable, A a subset of Act, and f : Act ! Act. The syntax of PCCS is given by: X X E ::= 0 j X j :E j pi] Ei where pi 2 (0; 1]; pi = 1 j E F j E A j E f ] j xX E
.. .. ..

Intuitively, 0 is the zero process having no transitions, while : E performs action with P probability 1 and then behaves like E . The expression pi ] Ei o ers a probabilistic choice among its constituent behaviors Ei. E F represents synchronized product, and the restricted expression E A can perform actions only from the set A. Finally, E f ] speci es a relabeling of actions, and xX E de nes a recursive process. A PCCS expression is guarded if in its syntactic tree, every path from a recursion operator xX to an occurrence of the corresponding variable X passes through an action operator :. In this paper we require expressions to be restriction-guarded, a much weaker requirement that ensures that the restriction operators in the generative and strati ed models are well-de ned. A PCCS expression is restriction-guarded if in its syntactic tree, every path from a recursion operator xX to an occurrence of the corresponding variable X either passes through an action operator :, or doesn't 1 1 pass through a restriction operator. This excludes expressions like xX ( 3 a:X + 1 b:X + 3 X fag) 3 but permits non-guarded expressions like xX (X f ] + (a:X ) fbg). We write E 2 PCCS to indicate that E is a restriction-guarded PCCS expression. An expression having no free variables is called a process, and Pr is the set of all restriction-guarded PCCS processes. For this paper, all summation expressions are required to be nite. It will be convenient to assume that all indices used in summation expressions come from a given set I0 not containing 0. Also, we write the binary version of process summation as p] E + 1 ? p] F , assuming an index set f1,2g, and often omit the square brackets around the probabilities.
.. .. . .. .. . .. . ..

i2I

i2I

7

:E ? E ?!

?! Ej ? E 0 ; j 2 I

=)

X
i2I

?! pi] Ei ? E 0
. .. . .

E ? E 0; F ? F 0 =) E F ????? E 0 F 0 ?! ?! ?! E ? E 0; 2 A ?! =) E A ? E 0 A ?!
. .. . .

E ? E0 ?! E f xX E=X g ? E 0 ?!

=) E f ] ????? E 0 f ] ?! =) xX E ? E 0 ?!
)

f(

Figure 4: Nonprobabilistic operational semantics of PCCS.

3 The Nonprobabilistic Model
We start with the nonprobabilistic model of PCCS based on Milner's model of SCCS Mil83]. In this model all probabilities are neglected and the only di erence between PCCS and SCCS is the di erent communication format. The reasons for including this section are to facilitate comparison between the probabilistic models and the classical one, and to present some proofs pertaining to classical bisimulation in such a way that they can be recycled in the probabilistic case.

3.1 Nonprobabilistic Operational Semantics of PCCS
The nonprobabilistic operational semantics of PCCS is given by the inference rules of Figure 4. We write N ` P ?! P 0 or just P ?! P 0 if P ?! P 0 can be derived from these rules. We refer to P ?! P 0 as a transition and its intuitive meaning is that P can perform action to become P 0. The rules of Figure 4 induce a mapping 'N from Pr to a domain of nonprobabilistic labeled transition systems.

De nition 1 A (nonprobabilistic) transition system is a triple (S,T,I) with { S a set of states, { T S Act S a set of transitions, { and I 2 S the initial state.
In a transition system all parts that are not reachable from the root as well as the identity of the states are often considered irrelevant. Therefore an isomorphism between two transition systems can be de ned as a bijective relation between their reachable states, preserving transitions and the initial state. Isomorphic transition systems are conceptually identi ed. Now 'N (P ) for P 2 Pr is de ned to be the transition system (S; T; I ) with S = Pr, I = P and T the set of transitions f(P; ; P 0) j N ` P ?! P 0g. 8

j j 'N : Pr ! GN to an interpretation of the open (restriction-guarded) PCCS expressions in GN , j N be the language PCCS to which all transition systems G 2 GN have been added as j let PCCS-G constants. We introduce an operational rule G ?! Gs for each initial transition (I; ; s) in each transition system G = (S; T; I ). Here Gs denotes the transition system with the same states and j transitions as G, but with s as the initial state. Let '0N be the extension of 'N to closed PCCS-GN expressions. Now let E be an open PCCS expression and a valuation of the free variables of j E in GN . Then denoting by E the result of substituting the constant (X ) for X in E , for all occurrences of free variables X in E , allows us nally to de ne 'N (E )( ) = '0N (E ). Note that the extended 'N in particular de nes an interpretation of the PCCS operators in j j GN , thereby making GN into a PCCS-algebra.

j Let GN be the domain of transition systems (or process graphs). To extend the mapping

3.2 Bisimulation
In this section we reformulate strong bisimulation Mil83] as bisimulation in the nonprobabilistic model, which we explicitly call nonprobabilistic bisimulation . A nonprobabilistic bisimulation will be presented as an equivalence relation over Pr. For this purpose we need a predicate that indicates whether or not from a given process it is possible to reach (a member of) a set of processes by means of an -step. Using P for the powerset operator we have:

De nition 2 The function Pr; 8S Pr;

: (Pr Act P (Pr)) ?! f0; 1g is given by: 8 2 Act; 8P 2 ( 1 if 9Q 2 S with P ?! Q N (P; ; S ) = 0 otherwise
N

For an equivalence relation R over Pr, we write Pr=R to denote the set of equivalence classes induced by R, and P ]R to denote the equivalence class of which P is a member. Nonprobabilistic bisimulation can now be de ned as follows:

De nition 3 An equivalence relation R Pr Pr is a nonprobabilistic bisimulation if (P; Q) 2 R implies: 8S 2 Pr=R; 8 2 Act, N (P; ; S ) = N (Q; ; S )
Two processes P; Q 2 Pr are nonprobabilistic bisimulation equivalent (written P N Q) if there exists a nonprobabilistic bisimulation R such that (P; Q) 2 R. Two open PCCS expressions E; F 2 PCCS are nonprobabilistic bisimulation equivalent i they are nonprobabilistic bisimulation equivalent after any substitution of closed terms for their free variables.

This de nition can easily be transformed into a de nition of bisimulation on transition systems (a bisimulation between two transition systems is a relation on the disjoint union of their states), such that, for E; F 2 PCCS, E N F () 8 valuations ; 'N (E )( ) N 'N (F )( ).

Proposition 1 If Ri (i 2 I ) is a collection of bisimulations, then also their re exive and transitive S closure ( i Ri) is a bisimulation.
9

Proof: Since each of the relations Ri is symmetric, (Si Ri) is also symmetric, and hence an S equivalence relation. Now suppose (P; Q) 2 ( i Ri ) . Then there are Pj (j = 0; . . . ; n) for certain n 2 IN, such that S = Po, Q = Pn and (for j = 1; . . . ; n) (Pj? ; Pj ) 2 Rk for certain k 2 I . P Suppose S 2 Pr=( i Ri) and 2 Act. Let 1 j n and (Pj ? ; Pj ) 2 Rk . Since S is the union of a number of equivalence classes T 2 Pr=Rk and N (Pj ? ; ; T ) = N (Pj ; ; T ) for any T 2 Pr=Rk , it follows that N (Pj? ;S ; S ) = N (Pj ; ; S ). This is true for all j = 1; . . . ; n; thus 2 N (P; ; S ) = N (Q; ; S ). Hence ( i Ri ) is a bisimulation.
1 1 1 1

Corollary 2 (Equivalence) Bisimulation equivalence is an equivalence relation on Pr. Proof: From the de nition of N it follows that on Pr we have N = f R j R is nonprobabilistic bisimulation g
Thus by Proposition 1, N is itself a bisimulation and hence an equivalence relation. 2 It is not di cult to see that a nonprobabilistic bisimulation is just a strong bisimulation Mil83, Mil89] that happens to be an equivalence relation. Since strong bisimulation equivalence, de ned as the union of all strong bisimulations, is an equivalence relation itself Mil83, Mil89], this is not a limiting restriction and nonprobabilistic bisimulation equivalence (being the union of all nonprobabilistic bisimulations) coincides with strong bisimulation equivalence. The following congruence theorem stems from Milner Mil83, Mil89]. Our proof is a bit di erent from Milner's because we insist that bisimulations should be equivalences and reason in terms of the function N rather than using the underlying transitions. This pays o when we add the probabilities. In the proof of the theorem, we lift the PCCS operators to sets of expressions, which is done in the natural way. For example, for S Pr, A Act, S A designates the set fP A j P 2 S g. A PCCS context is de ned as a PCCS expression that may contain a special constant . If C is a PCCS context and E a PCCS expression, then C E ] is the result of substituting E for all ] occurrences of in C , and C EX] (C ExX) is the result of substituting E for all occurrences of in x C that are (not) in the scope of an operator xX . Although we are only interested in contexts with exactly one \hole", i.e. one occurrence of , it is technically advantageous (in the congruence proofs) to also allow contexts without holes or with more than one hole. In C E ], though, all our holes are instantiated with the same expression E . The set of all restriction-guarded PCCS contexts is denoted PCCS ].
.. . .. . .. ..

:

Theorem 3 (Congruence) For E; F 2 PCCS, C 2 PCCS ]: E N F implies C E ] N C F ] Proof: The case of open PCCS expressions C E ]; C F ] can be reduced to the closed case, by considering C E ], C F ] under all possible substitutions. Note that for an expression C E ] any variable in E is either bound within E , free in E but bound within C E ], or free even in C E ].
Due to the de nition of bisimulation equivalence on open terms, we can eliminate from further consideration variables of the last kind, as well as free variables occurring in C . Now, adopting the 10

convention that \C 2 PCCS ] " should be read as \C 2 PCCS ] such that C E ]; C F ] 2 Pr", it is enough to show that the equivalence (i.e. re exive, symmetric, and transitive) closure R of R0 = f(C E ]; C F ]) j E N F; C 2 PCCS ] g is a bisimulation. This can be established by showing that for all (P; Q) 2 R, S 2 Pr=R and 2 Act, N (P; ; S ) = N (Q; ; S ) We may assume (P; Q) 2 R0, because the extension to the equivalence closure is straightforward. Thus we have to show that for all E; F 2 PCCS with E N F , 8C 2 PCCS ] ; 8S 2 Pr=R; 8 2 Act; N (C E ]; ; S ) = N (C F ]; ; S ) (1) We proceed by induction on the number of free variables in E and F . Let E; F 2 PCCS such that E N F , and suppose (1) is established for pairs E 0; F 0 2 PCCS with fewer free variables. Then it is enough to establish only one direction of (1), with substituted for =, as the converse direction, , follows by symmetry. Write N `n P ?! P 0 if the transition P ?! P 0 can be derived by a proof-tree of depth n or less, and de ne n : (Pr Act P (Pr)) ?! f0; 1g by: N ( n (P; ; S ) = 1 if 9Q 2 S with N `n P ?! Q N 0 otherwise Now N (P; ; S ) = nlim n (P; ; S ), so we only have to show that for all n 0, !1 N 8C 2 PCCS ] ; 8S 2 Pr=R; 8 2 Act; n (C E ]; ; S ) N (C F ]; ; S ) (2) N This will be done by induction to n. The case n = 0 is trivial, so we may assume (2) for a certain n 0. In proving (2) for n + 1 we distinguish seven cases, depending on the topmost operator (or lack thereof) of C . From here onwards we drop the subscripts N .

Empty context: We have to show that for all S 2 Pr=R and 2 Act,
n+1 (E;

Action pre xing: We have to show that for all C 2 PCCS ] , S 2 Pr=R and 2 Act, n ( : C E ]; ; S ) ( : C F ]; ; S )
+1

inequality.

; S ) (F; ; S ) (3) N is contained in the equivalence relation R. Thus S is the disjoint union of one or more T 2 Pr= N , and it su ces to prove (3) for these T instead of S . This follows immediately from E N F : n+1 (E; ; T ) (E; ; T ) = (F; ; T ) Note that at this point we cannot obtain (2) with the superscript n at both sides of the
(4)

1 if = and E 2 S 0 otherwise Thus, if 6= requirement (4) is ful lled trivially, and if = it follows since C E ] and C F ] are in the same equivalence class S 0 2 Pr=R. For any E 2 PCCS; n+1 ( : E; ; S ) = ( : E; ; S ) = 11

(

Summation: We have to show that for all Ci 2 PCCS ] , S 2 Pr=R and 2 Act, X n (X pi] Ci E ]; ; S ) ( pi] Ci F ]; ; S )
+1

i2I

i2I

(5)

Indeed, using LHS and RHS to denote the left- and right-hand sides of (5), we infer LHS = max( i2I
+1

n (C

i E ];

; S ))

induction

max( (Ci F ]; ; S )) = RHS i2I

Product: We have to show that for all Ci 2 PCCS ] (i = 1; 2), S 2 Pr=R and 2 Act, n (C E ] C E ]; ; S ) (C F ] C F ]; ; S ) (6) Since n (C E ] C E ]; ; S ? (Pr Pr)) = 0, we may in (6) replace S by S \ (Pr Pr). By the de nition of R we have (P ; P ) 2 R^ (Q ; Q ) 2 R ) (P Q ; P Q ) 2 R. Hence S \(Pr Pr) is the disjoint union of a collection of sets of the form S S with S ; S 2 Pr=R, and it su ces to prove (6) for such sets S S instead of S \ (Pr Pr). Moreover we may assume that is of the form ( ; ), since otherwise n (C E ] C E ]; ; S ) = 0 and we are done. Thus we have to show that for all Ci 2 PCCS ] , Si 2 Pr=R (i = 1; 2) and ; 2 Act, n (C E ] C E ]; ( ; ); S S ) (C F ] C F ]; ( ; ); S S )
1 2 1 2 +1 1 2 1 2 1 2 1 1 2 2 1 2 1 2 1 2 +1 1 2 +1 1 2 1 2 1 2 1 2

LHS = n (C1 E ]; ; S1 ) n (C2 E ]; ; S2 )
+1
. . .. .

induction

(C1 F ]; ; S1 ) (C2 F ]; ; S2) = RHS
.. .. .

Restriction: We have to show that for all C 2 PCCS ] , A Act, S 2 Pr=R and 2 Act, n (C E ] A; ; S ) (C F ] A; ; S ) (7) Since n (C E ] A; ; S ? Pr A) = 0, we may in (7) replace S by S \ (Pr A). By the de nition of R we have (P ; P ) 2 R ) (P A; P A) 2 R. Hence S \ (Pr A) is the disjoint union of a collection of sets of the form S 0 A with S 0 2 Pr=R, and it su ces to prove (7) for such sets S 0 A instead of S \ (Pr A). Moreover we may assume that 2 A, since otherwise n (C E ] A; ; S ) = 0 and we are done. Thus we have to show that for all C 2 PCCS ] , A Act, S 0 2 Pr=R and 2 A, n (C E ] A; ; S 0 A) (C F ] A; ; S 0 A)
+1
.. .. . .. .. . .. . ..

1

2

. .. ..

1

. .. . . .

2

. . . . .

. . . . .

.. . ..

. .. ..

+1

.. .. .

+1

.. .. .

.. .. .

.. .. .

.. . ..

LHS = n (C E ]; ; S 0)
+1

induction

(C F ]; ; S 0) = RHS

Relabeling: We have to show that for all C 2 PCCS ] , f : Act ! Act, S 2 Pr=R and 2 Act, n (C E ] f ]; ; S ) (C F ] f ]; ; S ) (8) Since n (C E ] f ]; ; S ? Pr f ]) = 0, we may in (8) replace S by S \ Pr f ]. By the de nition of R we have (P ; P ) 2 R ) (P f ]; P f ]) 2 R. Hence S \ Pr f ] is the disjoint union of a collection of sets of the form S 0 f ] with S 0 2 Pr=R, and it su ces to prove (8) for such sets
+1 1 2 1 2

12

S 0 f ] instead of S \ Pr f ]. Thus we have to show that for all C 2 PCCS ] , f : Act ! Act, S 0 2 Pr=R and 2 Act, n+1 (C E ] f ]; ; S 0 f ]) (C F ] f ]; ; S 0 f ])
LHS = fmax ( ( )=
n (C

E ]; ; S 0))

induction

f(

max ( (C F ]; ; S 0 )) = RHS )=

Recursion: We have to show that for all C 2 PCCS ] with xX C 2 PCCS ] , S 2 Pr=R and 2 Act, n ( x C E ]; ; S ) ( xX C F ]; ; S ) X
+1

In case X does not occur free in E or F this follows since LHS =
n (C

E ]f xX C E ]=X g; ; S ) = ; S) (Cf xX C =X g F ]; ; S ) = (C F ]f xX C F ]=X g; ; S ) = RHS

n (Cf x C =X g E ]; X

induction

In case X does occur free in E or F we have E f xX C F ]=X g N F f xX C F ]=X g by De nition 3, and since these expressions have fewer free variables than E and F it follows that (Cf xX C =X g F ] E f xX C F ]=X g]; ; S ) = (Cf xX C =X g FX] F f xX C F ]=X g]; ; S ) (9) x x X Hence LHS =
:

n (C

E ]f xX C E ]=X g; ; S ) =
(9)

n (C E ] f x C =X g E ]; X xX
:

; S)

induction

] (C ExXf xX C =X g F ]; ; S ) = (C F ]f xX C F ]=X g; ; S ) = RHS This argument is illustrated in Figure 5.

2

4 The Reactive Model
The reactive model of probabilistic processes was introduced by Larsen and Skou in LS91]. In this section, we consider the reactive model within the context of PCCSR, the sublanguage of PCCS with guarded recursion and without relabeling. We begin by presenting the reactive operational semantics for PCCSR that de nes a probabilistic transition system for every PCCSR process. We then equip the model with a notion of probabilistic bisimulation, also due to Larsen and Skou, and show that the resulting equivalence relation is a congruence with respect to PCCSR. We restrict ourselves to guarded recursion in order to ensure that the reactive summation operator is well-de ned. That we do not give a reactive semantics to the relabeling operator is due to an inherent incompatibility between this operation and the reactive viewpoint. For example, 1 consider process P = 1 a:X + 2 b:Y . P has a probability-1 a-transition to X and a probability-1 2 b-transition to Y . However, if the relabeling that maps a to itself and b to a is applied to P , then we may end up with a \nonsensical" object having two probability-1 a-transitions. Some form of relabeling could be de ned in the reactive model if an appropriate normalization procedure were 13

E X

F

C
X
xX xX

C

Two terms E and F , each with one free occurrence of a variable X

xX

E

E

xX

F

E

C C
xX xX

X

xX

C
xX

X

xX

X

E E X X

C
X E E X X
xX

X

F F X X

C
X F F X X
xX

X
and a context C with one free occurrence of X , one hole in the scope of an operator xX and one hole outside such a scope

Figure 5: The last steps in the congruence proof.

C E ]f xX C E ]=X g ] = C ExXf xX C =X g E ]
:

] C ExXf xX C =X g F ] = Cf xX C =X g FX] E f xX C F ]=X g] x
:

1 1 applied. Here three normalization procedures come to mind. Let Q = 1 a:X + 3 a:X + 6 b:Y + 1 c:Z 3 6 and again rename b into a. Now a \syntactic" normalization procedure would yield a probability- 1 5 a-transition to Y . This is also the solution obtained by abstracting from the generative or strati ed model (i.e. by applying 'GR 'G or 'SR 'S ), and from the counterexample in Section 7.1 it follows that this solution is not compositional. An intermediate normalization procedure would yield a probability- 1 a-transition to Y (by counting the number of summands that can do an a3 1 2 step). But then Q and Q0 = 3 a:X + 6 b:Y + 1 c:Z would behave di erently after relabeling, and 6 bisimulation equivalence would not be a congruence. Finally a \semantic" normalization procedure 1 would give the a-transition to Y probability 2 (by counting the number of actions that are renamed into a), but here the disadvantage is that rst renaming b in a and then c in a yields a di erent outcome than doing this in the reverse order. Of course, injective relabelings can be added without problem. A solution to the problem of de ning relabeling in the reactive model has recently been found

14

:E ??!0 E Ej ??!k E 0
p] q] p] q]

1]

=)

X
i2I

pi] Ei ??????! j:k E 0
p q]

pj q=r]

(

j 2 I; r =

X
i I
2

fjpi j Ei ??! l E jg)
00

s]

E ??!i E 0; F ??!j F 0 =) E F ??????! (i;j) E 0 F 0 E ??!i E 0 E f xX E=X g ??!i E 0
p] p] =) E A ??! i E 0 A
.. .. . .. . ..

=)

p] xX E ??!i E 0

( 2 A)

Figure 6: Reactive operational semantics of PCCSR. by Larsen and Skou personal communication]. They propose to equip a relabeling that renames actions a1 ; . . . ; an into a with a probability distribution that associates a probability pi to each of the ai 's. These probabilities then determine the normalization factor. As such a probabilistic relabeling is meaningless in the generative and strati ed models, we will not consider this solution in the present paper. The same problems encountered in de ning renaming in the reactive model apply to the SCCS product, as relabeling can be expressed in terms of product and the other SCCS operators. For this reason, we have \split" the SCCS product in the PCCS product and relabeling, only the latter of which has to be sacri ced in the reactive model.

4.1 Reactive Operational Semantics of PCCSR
The reactive operational semantics of PCCSR is given in Figure 6 as a set of inference rules. Reactive transitions are of the form meaning that P , with probability p, can perform an -transition to become P 0 . The index i is explained just below. In the second rule, in which fj; jg denote multiset brackets, r is the normalization factor used to compute the conditional probabilities of the sum under the assumption . The rest of the rules are straightforward adaptations of their nonprobabilistic counterparts. Unlike in the nonprobabilistic case, all probabilistic transitions are indexed. The set IR of reactive indices is the smallest set such that 0 2 IR , j 2 I0 ; k 2 IR ) j:k 2 IR , and i; j 2 IR ) (i; j ) 2 IR. The purpose of the indices is to distinguish di erent occurrences of the same probabilistic transition. They are constructed so that every outgoing probabilistic transition of an expression has a unique index. (The indices will be used in the next section to de ne cumulative

P ??!i P 0

p]

15

probability distributions.) The following example is illustrative: ( ]a : 0 + ]a : 0) ??! 1:0
1 2 1 2

a 1] 2

0

( ]a : 0 + ]a : 0) ??!2:0
1 2 1 2

a 1] 2

0

As in the nonprobabilistic case, the reactive operational rules collectively de ne the semantic mapping 'R from PrR , the closed expressions of PCCSR, and even from the open PCCSR expressions, to the domain of reactive probabilistic labeled transition systems.

De nition 4 A reactive (probabilistic) transition system is a triple (S,T,I) with { S a set of states, { T S Act (0; 1] IR S a set of transitions, such that 1. ((s; ; p; i; t) 2 T ^ (s; ; q; i; r) 2 T ) ) ( = ^ p = q ^ t = r) P 2. 8s 2 S; 8 2 Act; fjp j 9i 2 IR ; t 2 S : (s; ; p; i; t) 2 T jg 2 f0; 1g { and I 2 S the initial state.
The rst requirement of T says that all outgoing transitions of a given state have di erent indices. The second one says that for each state the probabilities of the outgoing -transitions, if there are any, sum up to 1, for any action separately. An isomorphism between two reactive transition systems is a bijective mapping f between their reachable states and transitions, satisfying f (s; ; p; i; t) = (f (s); ; p; j; f (t)), where i and j may be di erent indices, and f (I ) = I 0, where I and I 0 are the initial states of the two systems. The mapping 'R is de ned just as 'N in the previous section. It is not di cult to see that 'R (P ) meets the requirements for reactive transition systems.

4.2 Reactive Bisimulation
We now consider reactive bisimulation, a notion of probabilistic bisimulation for reactive processes due to Larsen and Skou LS91]. By de nition, all reactive bisimulations are equivalence relations. Intuitively, two processes P ,Q are probabilistically bisimilar in the reactive model if, for each action symbol, they derive reactive bisimulation classes with equal cumulative probability. To de ne reactive bisimulation, we rst need to de ne the cumulative probability distribution function (cPDF) which computes the total probability by which a process derives a set of processes. Adopting the convention that the empty sum of probabilities is 0, we have:

De nition 5 (Reactive cPDF) R: (PrR Act P (PrR)) ?! 0; 1] is the total function given by : 8 2 Act, 8 P 2 PrR , 8 S PrR ,
R (P;

; S) =

X
i2IR

fj pi jP ??!i Q and Q 2 S jg
16

pi ]

Reactive bisimulation can now be de ned as follows:

De nition 6 ( LS91]) An equivalence relation R (P; Q) 2 R implies : 8S 2 PrR=R; 8 2 Act,
R (P;

PrR PrR is a reactive bisimulation if ; S)

Two processes P; Q are reactive bisimulation equivalent (written P R Q) if there exists a reactive bisimulation R such that (P; Q) 2 R.

; S) =

R (Q;

By the same proof as was used for nonprobabilistic bisimulation, reactive bisimulation equivalence can be shown to be an equivalence relation indeed. Furthermore, reactive bisimulation equivalence is the largest reactive bisimulation and can be found by a straightforward adaptation of the xed-point iteration technique of Mil89]. Like strong bisimulation does for SCCS or CCS, reactive bisimulation equivalence provides a compositional semantics for PCCSR that is consistent with the operational semantics de ned in the last section. Speci cally:

remains after rst removing every subcontext of the form :E and subsequently every subcontext not containing . Now let PCCSk ] be the set of all PCCSR contexts with at most k nested R summation operators in their top. This time we have to show that for all E; F 2 PCCSR with E R F , and for all k 2 IN, (10) 8C 2 PCCSk ] ; 8S 2 PrR=R; 8 2 Act; R(C E ]; ; S ) = R(C F ]; ; S ) R This will be done by three nested inductions. First we apply induction on the number of free variables in E and F and choose E; F 2 PCCSR with E R F for the induction step. Then we apply induction on k and suppose (10) holds for k < l. Finally the proof of (10) for k = l continues exactly like the one for N (i.e. with induction on the depth of derivations), substituting R for N and PCCSlR ] for PCCS ], except that the function n : (PrR Act P (PrR)) ?! 0; 1] is given R by : 8 2 Act, 8 P 2 PrR , 8 S PrR , pi ] n (P; ; S ) = X fj p j R ` P ??! Q and Q 2 S j g i i n R and every time we invoke the induction hypothesis, we check that it is applied to contexts in PCCSlR ] only (in the case of recursion this follows by guardedness of PCCSR expressions). Moreover the case of relabeling is dropped|the congruence proof would break down where the operation max is applied|and the last line in the case of summation is replaced by: P P induction n C ; C i i R P fjp2Ijpi (CR (F i];F ];;Pr; S )6= 0jg = RHS LHS = P fjp2Ijpi (C (Ei];E ];;Pr S )6= 0jg R) R) i2I i R i i2I i R i (10)
i2IR

Theorem 4 (Congruence) For E; F 2 PCCSR, C 2 PCCSR ]: E R F implies C E ] R C F ] Proof: Following the previous congruence proof, we de ne R as the equivalence closure of R0 = f(C E ]; C F ]) j E R F; C 2 PCCSR ] g. The top of a context C 2 PCCSR ] is the part that

? Here (10) may be applied since Ci 2 PCCSlR 1 ] .

2

17

:E ? 0 E ?! Ej ? k E 0 ?!
p] q] p] q]

1]

=)

X
i2I

pi] Ei ????? j:k E 0 ?!
p q] p=r]

pj q ]

(j 2 I )

E ? i E 0; F ? j F 0 =) E F ????? (i;j) E 0 F 0 ?! ?! ?! E ? i E0 ?! E ? i E0 ?!
p]

?! =) E A ????? i E 0 A
. . . . . . . . . .

E f xX E=X g ? i E 0 ?!

p]

=) E f ] ????? i E 0 f ] ?! =)
xX E ? i E 0 ?!
p]

f ( ) p]

( 2 A ; r = G(E; A))

Figure 7: Generative operational semantics of PCCS.

5 The Generative Model
In contrast to the reactive model, which is de ned only over the sublanguage PCCSR of PCCS, the generative model is de ned over full PCCS. In this section, we provide PCCS with a generative operational semantics. We then extend the notion of reactive bisimulation to the generative case and show that the resulting equivalence is a congruence with respect to PCCS.

5.1 Generative Operational Semantics of PCCS
The generative operational semantics of PCCS is given in Figure 7. We use a di erent kind of arrow (non-hooked) to distinguish generative transitions from reactive ones. As in the reactive case, generative transitions are indexed to distinguish multiple occurrences of the same probabilistic transition. The set IG of generative indices is equal to IR . With the exception of restriction, all rules are straightforward adaptations of their nonprobabilistic counterparts. The restriction rule de nes the probabilistic transitions of E A in terms of the conditional probabilities of E under the assumption A. In this rule, the function G computes the generative normalization factor such that G (E; A) is the sum of the probabilities of the transitions of E labeled by symbols from A. The formal de nition of G is given by X p] fj pi j E ? i i Ei ; 2 Ajg ?! G (E; A) =
.. .. .

i2IG

Note that under the assumptions E ? i E 0 and 2 A, G (E; A) > 0. As we consider restriction?! guarded recursion only, it will follow from the proof of Theorem 5 that G is well-de ned. To illustrate the generative operational semantics, consider the expression 1 1 1 E = (a : 0) ( 3 ]b : X + 3 ]c : Y + 3 ]0) 18

p]

We have:

E ????? (0;1:0) 0 X ?!
(

1 a;b) 3 ]

E ????? (0;2:0) 0 Y ?!
(

1 a;c) 3 ]

As G (E; f(a; b)g) = 1 , we also have: 3

E f(a; b)g ????? (0;1:0) (0 X ) f(a; b)g ?!
. .. . .

(

a;b) 1]

. .. . .

A generative process is said to be stochastic if the sum of the probabilities of its derivations is 1. Otherwise, when this sum is strictly less than 1, the process is said to be substochastic, and therefore possesses a non-zero probability of deadlock. PCCS expressions (contexts) without 0, unguarded recursion and restriction preserve stochasticity : if stochastic processes are substituted for their free variables, then the obtained processes are stochastic as well. In the case of restriction, the obtained process may have no derivations at all. The normalization factor G (E; A) used in the restriction rule of Figure 7 is such that a substochastic process placed in a restriction context becomes stochastic or deadlocks completely. Alternatively, the relative probability of deadlock in a substochastic process can be preserved by normalizing by the quantity r = G (E; A) + 1 ? G (E; Act). The term 1 ? G (E; Act) represents the probability of deadlock in E . To illustrate, we would have in the above example that 2 2 G (E; Act) = 3 , r = 3 , and thus:

E f(a; b)g ?????2 (0;1:0) (0 X ) f(a; b)g ?!
. .. . .

(

a;b) 1 ]

. .. . .

In fact, deadlock preserving and eliminating restriction operators can be combined in one language by introducing an operator A for A Act f0g. From here on all results apply to this extended language. In Figure 7 the generative normalization factor is now extended by
.. .. .

G (E; A

.

0) = G (E; A) + 1 ? G (E; Act)
.. .. .

for A Act. In the reactive and nonprobabilistic models (A 0) is de ned exactly as A. A generative process is called semistochastic if the sum of the probabilities of its derivations is 0 or 1. PCCS expressions (contexts) without summation preserve semistochasticity, but a summation context, or an unguarded recursion context with summation, may introduce non-semistochastic behavior. Each of the expressions
.. .. .

.

1 2

a:0 + 1 0 2

and

2 xX ( 3 (X (a; b) ! a] X (a; b) ! b]) + 1 (a; b):X ) 3

1 for instance has a deadlock probability of 2 . PCCS may be turned into a semistochastic language by replacing the summation operator by a semistochastic variant, which can be expressed in our X language as ( pi] Ei) Act (using our deadlock eliminating restriction operator), and adapting
. .. ..

the de nition of restriction-guardedness. In this language there will be no di erence between the deadlock preserving and deadlock eliminating restriction operator, and p] X + 1 ? p] 0 X . 19

i2I

A generative transition system is de ned as a reactive transition system, except that the second requirement of T is changed into X 8s 2 S; fjp j 9 2 Act; i 2 IG; t 2 S : (s; ; p; i; t) 2 T jg 1 Also, the semantic mapping 'G from PCCS to the domain of generative transition systems is de ned exactly as 'N and 'R.

5.2 Generative Bisimulation
The extension of reactive bisimulation to the generative model is straightforward. The de nition of the generative cPDF G is the same as De nition 5 except that it is de ned over Pr and in terms of indexed generative transitions. Likewise, the de nition of a generative bisimulation and of G are the same as in De nition 6, except that they are de ned over Pr and in terms of G . Similar to the reactive case, G is substitutive in PCCS.

Theorem 5 (Congruence) For E; F 2 PCCS, C 2 PCCS ]: E G F implies C E ] G C F ] Proof: We follow the reactive congruence proof, but this time with PCCSk ] the set of PCCS contexts with at most k nested restriction operators in their top, until we have to show, for k 2 IN, 8C 2 PCCSk ] ; 8S 2 Pr=R; 8 2 Act; G (C E ]; ; S ) = G (C F ]; ; S ) (11)
Again, this will be done by induction on k. Suppose (11) holds for k < l. It then follows that

8k < l; 8C 2 PCCSk ] ; 8A Act . f0g; G (C E ]; A) = G (C F ]; A) because (restricting w.l.o.g. to the case A Act) X G (P; ; S ) G (P; A) =
S 2Pr=R
2

(12)

A

Now the proof of (11) for k = l continues just like the one for N , de ning n similar to n and G R substituting PCCSl ] for PCCSP except that the occurrences of max in the cases of summation ], and relabeling are replaced by (in the case of summation followed by pi ), and every time we invoke the induction hypothesis, we check that it is applied to contexts in PCCSl ] only (in the case of recursion this follows by restriction-guardedness of PCCS expressions). Moreover the last line in the case of restriction is replaced by: LHS =
n (C

E ]; ; S 0) induction (C F ]; ; S 0) = RHS (C E ]; A) (C F ]; A) (12) 2

Here (12) may be applied since C 2 PCCSl?1 ] . 20

X
i2I

pj pi] Ei 7?!j Ej

(j 2 I )

pq E 7?p i E 0; F 7?q j F 0 =) E F 7?!(i;j) E 0 F 0 ! ! p E 7?p i E 0; F ? F 0 =) E F 7?!(i;0) E 0 F ! ?! p p E ? E 0; F 7?!i F 0 =) E F 7?!(0;i) E F 0 ?! A E 7?p i E 0; E 0 ?! ! E 7?p i E 0 ! E f xX E=X g 7?p i E 0 !

=) E A ` ???????! i E 0 A =) E f ] 7?p i E 0 f ] ! =) xX E 7?p i E 0 !
. .. . . . .. . .

p= S (E;A)

Figure 8: Strati ed operational semantics of PCCS.

6 The Strati ed Model
The treatments of the nonprobabilistic, reactive and generative models are extended here to the strati ed case.

6.1 Strati ed Operational Semantics of PCCS
The strati ed operational semantics of PCCS is comprised of two types of transition relations: action transitions (as in the nonprobabilistic model) and probability transitions. Action transitions are of the form P ? Q. Probability transitions are of the form P 7?p i Q, meaning that P , with ?! ! 0 0 probability p, can behave as the process Q. Here i is an index from the set IS = IS ?f0g, where IS 0 0 0 0 is the smallest set such that 0 2 IS , I0 IS and i; j 2 IS ) (i; j ) 2 IS . This separation of action and probability in the strati ed model permits the branching structure of the purely probabilistic choices to be captured explicitly. The inference rules for probability transitions appear in Figure 8; the rules for action transitions are the same as in the nonprobabilistic case, except that there is no rule for process summation, since in the strati ed model the only choice mechanism is probabilistic. Only the probability transitions need to be indexed. This bi-structured approach to operational semantics was (to our knowledge) rst presented in Tof90a] to give a semantics for a timed version of CCS. Note that no PCCS expression admits both action and probability transitions. Thus the set of PCCS processes is partitioned into action processes (admitting action transitions), probability processes (admitting probability transitions), and deadlock processes (admitting neither). Except for the rules for product and restriction, all of the inferences rules for probability transitions are straightforward adaptations of their nonprobabilistic counterparts. The third and fourth rules say that the product of an action process and a probability process is a probability process. They are needed to avoid deadlock in a synchronous product that is caused by a di erence in depth of the purely probabilistic branching structures of the argument processes. For example, we do not 1 want ( 2 a:0 + 1 b:0) c:0 to deadlock simply because there does not exist a probability transition 2 in the right hand argument. 21

As in the generative operational semantics, the restriction rule expresses the probability transitions of E A in terms of the conditional probabilities of E under the assumption A. Intuitively, E A behaves like E , where all probability transitions to subexpressions that necessarily require the execution of a restricted action are eliminated. The probabilities associated with these transition are evenly distributed among the remaining probability transitions. p1 p2 pn A A ?! The predicate ?! for A Act is de ned by E ?! if E = E0 7?!i1 E1 7?!i2 7?!in En ? E 0 . Act . A f0g A for certain n 2 IN and 2 A. It is extended to A Act f0g by E ?! i (E ?! _E ?= ). ?! A Thus the condition E 0 ?! in the rule premise requires that derivative E 0 of E is capable of performing an action transition from the set A of permitted actions (or, in case 0 2 A, deadlocks). The function S calculates the strati ed normalization factor and is de ned by X A pi ?! fj pi j E 7?!i Ei ; Ei ? jg S (E; A) =
.. . .. .. .. .

i2IS

A As in the generative case, it will follow from the proof of Theorem 6 that ?! and S are well-de ned. To illustrate the inference rule for restriction, consider the process 1 1 P = 3 a:0 + 2 ( 2 b:0 + 1 c:0) 3 2 In the following, P is placed in some relevant restriction contexts, resulting in the restriction-free processes on the right-hand side.

P fb; cg P fa; cg P fcg
. .. . . .. .. . .. . . .

1 ( 1 b:0 + 1 c:0) 2 2 1 a:0 + 2 1 c:0 3 3 1 (1 c:0)

Here denotes isomorphism of the associated labeled transition systems. The inference rules for action and probability transitions de ne the semantic mapping 'S from PCCS to the domain of strati ed probabilistic labeled transition systems. Such transition systems have action states, having exactly one outgoing action transition, probability states, having only outgoing probability transitions, all with a di erent index, and deadlock states, having no outgoing transitions. Strati ed transition systems are semistochastic in the sense that for each probability state the sum of the probabilities of its outgoing transitions is 1. A state with a sequence of probability transition to a deadlocked state corresponds to a substochastic state in the generative model.

6.2 Strati ed Bisimulation
Strati ed bisimulation is similar to reactive and generative bisimulation in that processes are required to derive strati ed bisimulation equivalence classes with equal cumulative probability. However, the separation of probability and action in the strati ed operational semantics is re ected in the de nition of strati ed bisimulation. To de ne strati ed bisimulation, we need to: (1) de ne a function that computes the total probability by which a process can behave the same as any process in a set of processes (the 22

technique is analogous to the one in De nition 5, and thus the details are omitted); (2) lift, as in De nition 2, the action relations to sets of derivative processes. The strati ed cumulative PDF S incorporates both (1) and (2) in an integrated fashion. In particular, S is of the form
S

: (Pr (Act

f g) P (Pr)) ?! 0; 1]

where is a dummy symbol used to mark probability transitions. That is, for 2 Act; S (P; ; S ) 2 f 0; 1 g indicates whether or not P has an {transition to some process in S . Otherwise, S (P; ; S ) 2 0; 1] speci es the total probability by which P may behave the same as any process in S .

De nition 7 An equivalence relation R implies 8S 2 Pr=R; 8 2 Act f g,
S (P;

Pr Pr is a strati ed bisimulation if (P; Q) 2 R ; S ) = S (Q; ; S )

Two processes P; Q are strati ed bisimulation equivalent (written P S Q) if there exists a strati ed bisimulation R such that (P; Q) 2 R.

Theorem 6 (Congruence) For E; F 2 PCCS, C 2 PCCS ]: E S F implies C E ] S C F ] Proof: By induction on k (as in the generative case) we establish 8C 2 PCCSk ] ; 8S 2 Pr=R; 8 2 Act f g; S (C E ]; ; S ) = S (C F ]; ; S ) where R is de ned as usual. Suppose (13) holds for k < l. It then follows that
8k < l; 8C 2 PCCSk ] ; 8A Act . f0g; C E ] ?A i C F ] ?A ?! ?!
A A

(13) (14)

As a consequence we may write S ? for S 2 Pr=R when P ? for an arbitrary representative ?! ?! P 2 S . Now, if C E ] is not an action process, X S (C E ]; A) = S (C E ]; ; S )
A S ?!

and therefore

8k < l; 8C 2 PCCSk ] ; 8A Act . f0g;

S (C

E ]; A) = S (C F ]; A)

(15)

The proof of (13) for k = l is split into two cases. The case of an action transition 2 Act proceeds as the congruence proof for N , except that we check that the induction hypothesis is applied to contexts in PCCSl ] only, and in the case of summation we conclude with LHS = 0 = RHS. The case of a probability transition = also follows the proof for N , de ning n similar to S n , but with the following modi cations. R 23

Action pre xing: The proof of (4) (with = ) trivializes as n ( : C E ]; ; S ) = 0. Summation: The proof of (5) is replaced by n (X pi ] Ci E ]; ; S ) = X fjpi j Ci E ] 2 S j = X fjpi j Ci F ] 2 S j = (X pi ] Ci F ]; ; S ) g g
+1 +1

i2I

i2I

i2I

i2I

since, for i 2 I , Ci E ] and Ci F ] are in the same equivalence class S 0 2 Pr=R. Product: The proof of (6) (with = ) is unchanged until \Moreover". Then we have to show that for all Ci 2 PCCSl ] and Si 2 Pr=R (i = 1; 2),
n+1 (C1 E ]

C E ]; ; S
2

1

S2 )

(C1 F ] C2 F ]; ; S1 S2 )

(16)

For this we distinguish 4 cases, depending on whether or not C1 E ] and C2 E ] are probability processes. If neither of them are, (16) follows since LHS=0. If both of them are, we have LHS = n (C1 E ]; ; S1 ) n (C2 E ]; ; S2 )
induction

(C1 F ]; ; S1) (C2 F ]; ; S2) = RHS

And if just one of them (say C1 E ]) is a probability process, (16) follows since
induction X n X LHS = n (C1 E ]; ; S1) (C2 E ]; ; S2) (C1 F ]; ; S1) (C2 F ]; ; S2) = RHS
2Act 2Act

Restriction: The proof of (7) is unchanged until \Moreover". Then we have to show that for all C 2 PCCSl ] , A Act f0g and S 0 2 Pr=R, n (C E ] A; ; S 0 A) (C F ] A; ; S 0 A) (17)
+1
. . .. . . .. . . . .. . . . .. . .

Now the proof of (17) proceeds with a case distinction. In case S 0 ?/ we have LHS=0=RHS. ?! 0 ?A it concludes as in the generative case. In case S ?! Relabeling: This case (with = ) concludes with LHS = n (C E ]; ; S 0)
induction

A

(C F ]; ; S 0) = RHS 2

7 Interrelating the Models
In this section we establish the results announced in the introduction, showing that the models discussed before form a hierarchy. We start with investigating the abstraction from the generative to the reactive model in Section 7.1, followed by an analogous treatment of the more intricate abstraction from the strati ed to the generative model in Section 7.2. Subsequently, we give a direct abstraction from the strati ed to the reactive model in Section 7.3. Finally, we brie y sketch the simpler abstraction steps leading from probabilistic to nonprobabilistic models. 24

7.1 The Generative to Reactive Abstraction
Let E; E 0 be PCCS expressions. The inter-model abstraction rule IMARGR is de ned by

E ? i E 0 =) E ??????! i E 0 ?!
This rule uses the generative normalization function to convert generative probabilities to reactive ones, thereby abstracting away from the relative probabilities between di erent actions. We can now de ne 'GR ('G (P )) as the reactive transition system that can be inferred from P 's generative transition system via IMARGR . By the same procedure as described at the end of Section 3.1, 'GR j j can be extended to a mapping 'GR : GG ! GR . Write P GR Q if P; Q 2 Pr are reactive bisimulation equivalent with respect to the transitions derivable from G + IMARGR , i.e. the theory obtained by adding IMARGR to the rules of Figure 7. The equivalence GR is de ned just like R but using the cPDF GR instead of R . GR is de ned by pi ] X (P; ; S ) = fj pi j G + IMARGR ` P ??!i Q and Q 2 S jg GR
i2IR (=IG )

p]

p= G(E;f g)]

j Theorem 7 (Abstraction) Let G; H 2 GG. Then G G H ) 'GR(G) R 'GR(H ).

Proof: We prove this theorem for the case that G and H are of the form 'G(P ) and 'G(Q) with P; Q 2 Pr and use that 'G(P ) G 'G(Q) , P G Q and 'GR('G(P )) R 'GR('G(Q)) , P GR Q.
The proof of the general case is not essentially di erent, but would involve de ning the reactive and generative bisimulation equivalences formally on transition systems. Let R be a generative bisimulation on Pr. We prove that R is also a reactive bisimulation on Pr with respect to the transitions derivable from G + IMARGR. So let (P; Q) 2 R, S 2 Pr=R and 2 Act. Then X X G (P; f g) = G (P; ; S ) = G (Q; ; S ) = G (P; f g); so
S 2Pr=R S 2Pr=R GR (P;

; S) =

G (P; ; S ) = G (Q; ; S ) = GR (Q; G (P; f g) G (Q; f g)

; S) 2

We will now investigate to what extent 'GR commutes with the semantic mappings 'G and 'R. This turns out to be the case for PCCSR processes in which all summations are of the form X pi] i : Ei. We say that such an expression is summation-guarded.
i2I

Lemma 1 (Soundness and Completeness of IMARGR ) For E; E 0 summation-guarded PCCSR expressions, 2 Act, p 2 (0; 1] and i 2 IR ,
R ` E ??!i E 0 () G + IMARGR ` E ??!i E 0
25
p] p]

Proof: As in the congruence proofs, we use induction on the depth of derivation trees, and write p p R `n E ??!i E 0 if the transition E ??!i E 0 can be derived by a proof-tree of depth n. In the similar de nition of G + IMARGR `n we don't count the single application of IMARGR though.
] ]

We distinguish several cases, depending on the topmost operator of E . The case of action pre xing is trivial. X j q] pi] i : Ei ??????! j Ej Guarded summation: R `2 i2I X X pk = pj / G ( pi] i : Ei; f j g) i j 2 I and q = pj / i2I k2I; k = j X j q] pi] i : Ei ??????! j Ej . i G + IMARGR `2
i2I
(

Product: R `n E F ??????! i;j E 0 F 0 p q i R `n E ??????! i E 0; F ??????! j F 0 and p q = r p q i G + IMARGR `n E ??????! i E 0; F ??????! j F 0 and p q = r (by induction) p G E;f g q G F;f g i G `n E ????? i E 0; F ????? j F 0 and p q = r ?! ?! ; rs i G `n E F ????? i;j E 0 F 0 and s = G (E; f g) G (F; f g) = G (E F; f( ; )g) ?! ; r i G + IMARGR `n E F ??????! i;j E 0 F 0 .
+1 ( ) ] ] ] ] ( )] ( )] ( ) ] +1 ( ) ( ) ] +1 ( )

; ) r]

Restriction: R `n E A ??????! i E 0 A p i R `n E ??????! i E 0 and 2 A p i G + IMARGR `n E ??????! i E 0 and 2 A (by induction) p G E;f g i G `n E ????? i E 0 and 2 A ?! pr ?! i G `n E A ????? i E 0 A where r = GGE;f g = G (E A; f g) E;A p i G + IMARGR `n E A ??????! i E 0 A.
+1
.. .. . .. .. .

p]

]

]

(

)]

+1

. .. ..

]

.. . ..

(

)

.. .. .

(

)

+1

.. .. .

]

.. . ..

Recursion: R `n xX E ??????! i E 0 p i R `n E f xX E=X g ??????! i E 0 p i G + IMARGR `n E f xX E=X g ??????! i E 0 (by induction) pr i G `n E f xX E=X g ????? i E 0 where r = G (E f xX E=X g; f g) = G ( xX E; f g) ?! p G xX E;f g i G `n xX E ????? i E 0 ?! p i G + IMARGR `n xX E ??????! i E 0. 2
+1 ] ] ] ( )] +1 ] +1

p]

As an immediate consequence of Lemma 1 we have: 26

Theorem 8 (Commutativity) Let P 2 PrR be summation-guarded. Then 'GR('G(P ))= 'R(P ). Corollary 9 Let P; Q 2 PrR be summation-guarded. Then P G Q ) P R Q. Proof: Theorem 7 says that P G Q ) P GR Q for P; Q 2 Pr. Theorem 8 (or Lemma 1) implies R GR Q for summation-guarded P; Q 2 Pr . 2 R (P; ; S ) = GR (P; ; S ) and hence P Q , P R
Theorem 8 does not hold in the presence of general summation. Consider the process
1 1 P = 3 a : X + 2 ( 1 a : Y + 2 b : Z) 3 2

In 'GR ('G (P )) the probabilities of a:X and a:Y are equal, while in 'R (P ) executing a:Y is twice as likely as a:X . This counterexample can be easily extended so to apply to Corollary 9 as well. One may wonder whether relabeling could be added to, or summation rede ned on the reactive model such that reactive bisimulation remains a congruence, but Theorem 8 can be extended. This is not possible as it would imply that GR is a congruence, which will be refuted below. The equivalence GR (which was previously de ned only on closed PCCS expressions) can be extended to arbitrary generative labeled transition systems by G GR H , 'GR (G) R 'GR (H ), and P GR Q , 'G (P ) GR 'G (Q). We show that this equivalence is not a congruence, thus demonstrating the need for re ning the bisimulation semantics when moving from the reactive to the generative model. Consider the PCCS processes 1 P = 1a : 0 + 2b : c : 0 Q = 2a : 0 + 1b : c : 0 3 3 2

'GR('G(P )) R 'GR('G(Q)) However, the same is not true for C P ] and C Q], where C is the relabeling a ! a; b ! a; c ! c]. In particular, GR (C P ]; a; c : 0] R ) = 2 and GR (C Q]; a; c : 0] R ) = 1 . 3 2 A similar counterexample is obtained by placing P and Q in the summation context C = 1 2 ] + 1 b : 0. In this case GR (C P ]; b; c : 0] R ) = 5 and GR (C Q]; b; c : 0] R ) = 2 . 2 2 3

For P ,Q we have P GR Q, i.e.

7.2 The Strati ed to Generative Abstraction
Let E; E 0 be PCCS expressions. Then IMARSG is given by

E ? E 0 =) E ? 0 E 0 ?! ?!
1]

where i:j (as in the generative case) denotes the concatenation of two indices. Thus the elements of ISG , the set of indices generated by S + IMARSG , are sequences, and we let jij denote the length of such a sequence. 27

p E 7?!i E 0 ? j E 00 =) E ????? i:j E 00 ?! ?!

q]

p q]

Write P SG Q if P; Q 2 Pr are generative bisimulation equivalent with respect to the transitions derivable from G + IMARSG . The equivalence SG is de ned just like G , but using the cPDF SG instead of G . SG is de ned by X p] fj pi j G + IMARSG ` P ? i i Q and Q 2 S jg ?! SG (P; ; S ) =
i2ISG

j Theorem 10 (Abstraction) Let G; H 2 GS . Then G S H ) 'SG (G) G 'SG(H ).

Proof: As before, we prove this theorem for the case that G and H are of the form 'S (P ) and 'S (Q). Thus we show that for P; Q 2 Pr, P S Q ) P SG Q.
We now de ne
n (P; SG

; S) =

X
i2ISG

fj pi j S + IMARSG ` P ? i i Q; Q 2 S and jij = njg ?!

p]

Let R be a strati ed bisimulation on Pr. We prove that R is also a generative bisimulation on Pr with respect to the transitions derivable from S + IMARSG , i.e. that for (P; Q) 2 R, S 2 Pr=R and 2 Act, SG (P; ; S ) = SG (Q; ; S ) P As SG (P; ; S ) = n2IN n (P; ; S ), it su ces to prove this for every n , which we will do by SG SG induction on n. 1 1 SG (P; ; S ) = S (P; ; S ) = S (Q; ; S ) = SG (Q; ; S )
n+1 (P; SG

; S) =

X
i2IS ;j 2ISG

i fj pi qj j S +IMARSG ` P 7?p!i R ? j Q; R 2 Pr; Q 2 S and jj j = njg ?!

qj

= = =

X
R2Pr

S (P;

X

X
R] 2Pr=R
R

R] 2Pr=R
R

; S) independent of choice of R 2 R]R n (R. ; S ) S (P; ; R]R) SG ;
n (R; SG

; fRg)

n (R; SG

S (Q;

; R]R)

; S) =

n+1 (Q; SG

; S) 2

IMARSG has the e ect of \ attening" trees of probability transitions with action transitions at the leaves, into a single-level structure of generative transitions. Indeed, we show that the generative transition system of a restriction-free PCCS process P is isomorphic to the generative transition system that can be inferred from P 's strati ed transition system via IMARSG . For example, let 1 1 P = 3 a : 0 + 2 ( 1 b : 0 + 2 c : 0). Then, by IMARSG 3 2

P ? 2:2:0 0 ?! Except for the transition indices, these are precisely the transitions of P in the generative model.
28

P ? 1:0 0 ?!

1 a 3]

P ? 2:1:0 0 ?!

b 1] 3

1 c 3]

Lemma 2 (Soundness and Completeness of IMARSG ) There is a surjection f : IG ! ISG such that for E; E 0 restriction-free PCCS expressions, 2 Act, p 2 (0; 1] and i 2 IG ,
G ` E ? i E 0 () S + IMARSG ` E ? f (i) E 0 ?! ?!
Moreover G ` E ? i E 0; E ? j E 00; i 6= j =) f (i) 6= f (j ). ?! ?!
p] q] p] p]

Proof: In Lemma 1 f happened to be the identity function and was therefore not mentioned.
0

Unfortunately, f can not be chosen bijective this time. In order to get rid of this complication in an early stage, we split the proof in two parts by considering an intermediate operational semantics G0. The inference rules of G0 are exactly the same as the ones of G, except that in the rule for product when i and j are both 0 the resulting index is also 0 instead of (0; 0). Let f 0 : IG ! IG be the function that exhaustively replaces all occurrences of (0; 0) in an index by 0. Then

G ` E ? i E 0 () G0 ` E ? f (i) E 0 ?! ?!
0

p]

p]

Now let G ` E ? i E 0; E ? j E 00 and f 0 (i) = f 0 (j ). If E is summation-free, it has only ?! ?! one outgoing transition and therefore i = j . Otherwise i = j is established by a straightforward induction on the length of derivations. We refer to this property of f 0 as \limited injectivity" since f 0 is injective only with respect to the transition indices of a given E . The second part of the proof consist of establishing Lemma 2 with G0 instead of G and f : IG ! ISG . This function can be chosen bijective. 0 0 0 Recall that IS = IS f0g and let ISG be the largest set of sequences over IS such that an index 0 (i; j ) can only be followed by either 0 or an index (k; l) such that i:k; j:l 2 ISG , and an index 0 can 0 only be followed by an index 0. Then ISG = ISG \ (IS ) 0. This follows from the fact that product is a static operator, i.e. the syntactic subtree of occurrences of product in a PCCS expression is 0 preserved under strati ed derivations. De ne head : IG ! IS , tail : IG ! IG and the partial 0 function : IS IG ! IG by
0 0 0 0 0 0

p]

q]

head(0) = 0 tail(0) = 0 head(i:j ) = i tail(i:j ) = j( head(i; j )=(head(i); head(j)) tail(i; j ) = (tail(i); tail(j)) if 6= (0; 0) 0 otherwise

i j = i:j (i 2 I0) (i; j ) (k; l) = (i k; j l) (i; j ) 0 = (i 0; j 0)

0 0=0

With structural induction on j for \)" and on i for \(" it follows that

i = j k , j = head(i) ^ k = tail(i) (18) Moreover, if i 6= 0, head(i) 2 IS and tail(i) is a shorter index than i. De ne f : IG ! ISG by ( if i = 0 f (i) = 0 (i) : f (tail(i)) otherwise head and g : ISG ! IG by g(i0: :in) = (i0 ( (in?1 in) ))
0 0

29

Note that f transforms pairs of sequences into sequences of pairs. Clearly f (i) 2 ISG for i 2 IG and g(i) 2 IG for i 2 ISG . Further g is the inverse of f by (18), and hence f is bijective. The bijectivity of f together with the limited injectivity of f 0 establishes the \moreover" part of the lemma.
0 0

We now proceed to prove

is almost no di erence between the generative and strati ed (=nonprobabilistic) inference rules, and the statement holds. In case i 6= 0 we again use induction on the depth of derivation trees, albeit modi ed ones. Here the modi cation of a G0 derivation tree consists of removing all ancestors of transitions from summation expressions, and the modi cation of an S +IMAR SG derivation tree consists of erasing any subtree ending with a clause that is used as the second argument in an application of IMARSG . Moreover, the remaining application of IMARSG doesn't count. We now use the notation `n to refer to the depth of modi ed derivations, and prove by induction on n. We distinguish several cases, depending on the topmost operator of E . As i 6= 0 this operator cannot be action pre xing. X p] q] pi] Ei ????? j:k E 0 i G0 ` Ej ????? k E 0 and p = pj q Summation: G0 `1 ?! ?! i
i2I S + IMARSG ` Ej

G0 ` E ? i E 0 () S + IMARSG ` E ? f (i) E 0 ?! ?! by structural induction on i. In case i = 0 (the induction base) E must be summation-free and there

p]

p]

G0 `n E ? i E 0 () S + IMARSG `n E ? f (i) E 0 ?! ?!

p]

p]

i S + IMARSG `1

X
i2I

????? f k E 0 and p = pj q (by induction (k < j:k)) ?!
( )

q]

pi] Ei ????? f (j:k) E 0 (since S `1 ?!
(

p]

X
i2I

pi] Ei ` ???????! j Ej ).

pj

Product: In case i 6= 0 6= j : G0 `n E F ????? i;j E 00 F 00 ?! p q i G0 `n E ????? i E 00; F ????? j F 00 and p q = r ?! ?! p q i S + IMARSG `n E ????? f i E 00; F ????? f j F 00 and p q = r (by induction) ?! ?! q1 p1 ???????! head i E 0; F `???????! head j F 0, i S `n E ` p2 q2 S + IMARSG ` E 0 ? f tail i E 00; F 0 ? f tail j F 00 and p p q q = r ?! ?! p1 q1 i S `n E ` ???????! head i E 0; F `???????! head j F 0, p2 q2 G0 ` E 0 ? tail i E 00; F 0 ? tail j F 00 and p p q q = r (by induction) ?! ?! r i S `n E F ` 1 ???????! head i ;head j E 0 F 0, ; r2 G0 ` E 0 F 0 ????? tail i;j E 00 F 00 and r r = r ?! r i S `n E F ` 1 ???????! head i;j E 0 F 0, ; r2 S + IMARSG ` E 0 F 0 ????? f tail i;j E 00 F 00 and r r = r (by induction) ?! ; r i S + IMARSG `n E F ????? f i;j E 00 F 00 . ?!
+1 ( ) ] ] ] ] ( ) ( ) ( ) ] ( ) ( ] ( ( )) ( )) 1 2 1 2 ( ) ( ) ] ] ( ) ( ) 1 2 1 2 +1 ( ( ) ( )) ( ) ] ( ) 1 2 +1 ( ) ( ) ] ( ( )) 1 2 ( ) ] +1 ( )

; ) r]

30

In case i 6= 0 = j : G0 `n+1 E F ????? (i;0) E 00 F 00 ?! r] 1] i G0 `n E ????? i E 00; F ????? 0 F 00 ?! ?! r] 1] i S + IMARSG `n E ????? f (i) E 00; F ????? 0 F 00 (by induction) ?! ?!
(

; ) r]

i S `n E ` 1 ???????! head(i) E 0; F ????? F 00, ?! r2 ] 1] S + IMARSG ` E 0 ????? f (tail(i)) E 00; F ????? 0 F 00 and r1 r2 = r ?! ?!

r

???????! head(i) E 0; F ????? F 00, ?! i S `n E ` 1 r2 ] 1] G0 ` E 0 ????? tail(i) E 00; F ????? 0 F 00 and r1 r2 = r (by induction) ?! ?! r i S `n+1 E F ` 1 ???????! (head(i);0) E 0 F , ( ; ) r2] G0 ` E 0 F ????? tail(i;0) E 00 F 00 and r1 r2 = r ?! r i S `n+1 E F ` 1 ???????! head(i;0) E 0 F , ( ; ) r2] S + IMARSG ` E 0 F ????? f (tail(i;0)) E 00 F 00 and r1 r2 = r (by induction) ?! ( ; ) r] i S + IMARSG `n+1 E F ????? f (i;0) E 00 F 00. ?! The case i = 0 6= j is symmetric.

r

Relabeling: G0 `n E f ] ????? i E 00 f ] ?! p i G0 `n E ????? i E 00 and f ( ) = ?! p i S + IMARSG `n E ????? f i E 00 and f ( ) = (by induction) ?! p2 p1 i S `n E 7?!head i E 0, S + IMARSG ` E 0 ? f tail i E 00, p p = p and f ( ) = ?! p2 p1 i S `n E 7?!head i E 0, G0 ` E 0 ? tail i E 00, p p = p and f ( ) = (by induction) ?! p2 p1 i S `n E f ] 7?!head i E 0 f ], G0 ` E 0 f ] ? tail i E 00 f ], p p = p ?! p2 p1 i S `n E f ] 7?!head i E 0 f ], S + IMARSG ` E 0 f ] ? f tail i E 00 f ], p p = p (ind.) ?! p i S + IMARSG `n E f ] ????? f i E 00 f ]. ?!
+1 ] ] ( ) ] ( ) ( ( )) 1 2 ] ( ) ( ) 1 2 ] +1 ( ) ( ) 1 2 ] +1 ( ) ( ( )) 1 2 ] +1 ( )

p]

Recursion: G0 `n xX E ????? i E 00 ?! p i G0 `n E f xX E=X g ????? i E 00 ?! p i S + IMARSG `n E f xX E=X g ????? f i E 00 (by induction) ?! p2 p1 i S `n E f xX E=X g 7?!head i E 0; S +IMARSG ` E 0 ????? f tail i E 00 and p p = p ?! p2 p1 i S `n xX E 7?!head i E 0; S + IMARSG ` E 0 ????? f tail i E 00 and p p = p ?! p i S + IMARSG `n xX E ????? f i E 00. ?! 2
+1 ] ] ( ) ] ( ) ( ( )) 1 2 ] +1 ( ) ( ( )) 1 2 ] +1 ( )

p]

As an immediate consequence of this lemma, we obtain the following commutativity result: 31

Theorem 11 (Commutativity) Let P 2 Pr be restriction-free. Then 'SG('S (P )) = 'G (P ). Corollary 12 Let P; Q 2 Pr be restriction-free PCCS processes. Then P S Q ) P G Q. Proof: Theorem 10 says that P S Q ) P SG Q for P; Q 2 Pr. Theorem 11 (or Lemma 2) implies G SG Q for restriction-free P; Q 2 Pr. 2 G (P; ; S ) = SG (P; ; S ) and hence P Q , P
Theorem 11 does not hold for arbitrary PCCS processes. Consider the process 1 1 P = 3 a : 0 + 2 ( 2 b : 0 + 1 c : 0) fa; bg 3 2 1 1 'G(P ) is equal to 2 a : 0 + 2 b : 0 while 'SG ('S (P )) is equal to 1 a : 0 + 2 b : 0. 3 3 This counterexample can be easily extended so to apply to Corollary 12 as well. However, Theorem 11 and Corollary 12 do hold for summation-guarded PCCS processes with restriction. The reason is that for those processes there is hardly any di erence between the generative and strati ed models. It su ces to extend Lemma 2 to this case.
.. .. .

Lemma 3 Lemma 2 also holds for summation-guarded PCCS expressions.
concerning the induction base still holds. For the induction step we use that in the strati ed model, if E is summation-guarded and E 7?p i E 0, then E 0 is an action process. This can be inferred by ! a straightforward induction on strati ed derivations. It follows that G (E; A) = S (E; A).

Proof: It su ces to add the case for restriction to the proof of Lemma 2. Check that the remark
p]

Restriction: G0 `n E A ????? i E 00 A ?! p G E;A i G0 `n E ????? i E 00 and 2 A ?! p G E;A i S + IMARSG `n E ????? f i E 00 and 2 A (by induction) ?! p S E;A ???????! head i E 0; f (tail(i)) = 0; S ` E 0 ? E 00 and 2 A ?! i S `n E ` p ?! i S `n E A 7?!head i E 0 A; S + IMARSG ` E 0 ? f tail i E 00 and 2 A p i S + IMARSG `n E A ????? f i E 00 A. ?!
+1
.. .. . . .. ..

(

)]

(

)]

( )

(

)

( )

+1

.. .. .

( )
.. .. .

.. . ..

1]

(

( ))

]

+1

( )

.. .. .

2

Finally, we show that the equivalence induced on the strati ed model by generative bisimulation is not a congruence for restriction. Consider processes Sc and Sc0 of Section 1 (the scheduler speci cations). We have 'SG ('S (Sc)) G 'SG ('S (Sc0)) but, as discussed in Section 1, 'SG ('S (Sc fa; bg)) 6 G 'SG ('S (Sc0 fa; bg)).
.. .. . .. .. .

7.3 The Strati ed to Reactive Abstraction
Let E; E 0 be PCCS expressions. Then IMARSR is given by

E ? E 0 =) E ??!0 E 0 ?!
32

1]

E

7?!i E 0

p

??!j E 00 =)

q]

E ??????! i:j E 00
f g

pq S (E;

)]

j j This inter-model abstraction rule de nes a mapping 'SR : GS ! GR . Like the composed mapj S ! GR , 'SR attens trees of probability transitions with action transitions at j ping 'GR 'SG : G the leaves into a single-level structure, and normalizes the probabilities to yield a reactive transition system. However, whereas 'GR 'SG rst attens and then normalizes, 'SR performs these operations interactively. From the proof of Lemma 3 it follows that for summation-guarded PCCS expressions there is no di erence between both approaches. But in general the two mappings are di erent, as will be demonstrated at the end of this section. j Theorem 13 (Abstraction) Let G; H 2 GS . Then G S H ) 'SR(G) R 'SR(H ).

Proof: Combine the proofs of Theorems 10 and 7. (It doesn't su ce to combine just the theorems themselves since 'GR 'SG (G) = 'SR (G) for an arbitrary strati ed transition system G). 6 2 Theorem 14 (Commutativity) Let P 2 PrR. Then 'SR('S (P )) = 'R(P ). Proof: We proceed along the lines of the proof of Theorem 11 (i.e. Lemma 2), substituting R's for
G's, but with the following modi cations in the cases for the topmost operator of E . X s] X 00j = S ( pi] Ei; f g). Summation: p = pj q=r where r = fjpi j Ei ??!l E g
i2I
1

i2I

Product: In case i 6= 0 6= j : p p q q = r S (E; f g) S (F; f g) = r and r r = r S (E F; f( ; )g). In case i = 0 = j : r r = r S (E; f g) = r S (E F; f( ; )g). 6
1 2 2 1 2 1 2 +1
.. . . .

S (E

F; f( ; )g)

Restriction: R0 `n E A ??????! i E 00 A p i R0 `n E ??????! i E 00 and 2 A p i S + IMARSR `n E ??????! f i E 00 and 2 A (by induction) p2 p1 i S `n E 7?!head i E 0, S +IMARSR ` E 0 ??! f tail i E 00, p p = p S (E; f g) and 2 A p2 p1 i S `n E 7?!head i E 0, R ` E 0 ??!tail i E 00, p p = p S (E; f g) and 2 A (induction) p2 r1 i S `n E A 7?!head i E 0 A, R ` E 0 A ??!tail i E 00 A and r p = p SS E;f g E;A p2 r1 i S `n E A 7?!head i E 0 A, S +IMARSR ` E 0 A ??! f tail i E 00 A, r p = p S (E A; f g) p i S + IMARSR `n E A ??????! f i E 00 A. Relabeling: This case does not apply as E is a PCCSR expression. Recursion: p p = p S (E f xX E=X g; f g) = p S ( xX E; f g). 2
.. .. .

p]

]

]

( )

]

( )

(

( ))

1

2

]

( )

( )
.. . ..

1

2

+1

. .. ..

( )

.. .. ..

]

( )

. .. ..

1

2

(

)

(

)

+1

.. .. .

( )

.. . ..

. .. ..

]

(

( ))

.. .. .

1

2

. .. ..

+1

.. . ..

]

( )

.. . . .

1

2

33

Corollary 15 Let P; Q 2 PrR. Then P S Q ) P R Q.
By means of the same counterexample that we used at the end of Section 7.1, one shows that the equivalence induced on the strati ed model by reactive bisimulation through 'SR is not a congruence for relabeling. As a consequence, no compositional de nition of relabeling in the reactive model is possible that allows a generalization of Theorem 14. The corresponding counterexample for summation is also valid for 'GR 'SG , but not for 'SR (in fact, it couldn't be, by Theorems 14 and 4). Hence these two mappings are di erent. It appears that 'SR preserves some of the strati ed avor of nested PCCS summations, which is lost by 'GR 'SG .

7.4 The Probabilistic to Nonprobabilistic Abstraction
Let E; E 0 be PCCS expressions. Then IMARSN is given by

E 7?p i E 0 ? E 00 =) E ? E 00 ! ?! ?!
Similarly IMARGN and IMARRN are given by

E ? i E 0 =) E ? E 0 ?! ?! E ??!i E 0 =) E ? E 0 ?!
These inter-model abstraction rules simply throw away all probabilities. It is comparatively straightforward to establish the remaining commutativity results announced in the introduction.
j Theorem 16 (Abstraction) Let G; H 2 GR. Then G R H ) 'RN (G) N 'RN (H ).
p]

p]

Proof: Following the idea of the previous abstraction proofs, we show that a reactive bisimulation on PrR is also a nonprobabilistic bisimulation (with respect to the transitions derivable from R + IMARRN , but by commutativity these are the same as the ones derivable from N ). This follows as N is completely determined by R , namely ( 0 if R (P; ; S ) = 0 2 N (P; ; S ) = 1 if (P; ; S ) > 0
R

As before, the general (semantic) case can be obtained in the same way, after de ning the involved bisimulations on the (semantic) transition system domains. Generative or strati ed to nonprobabilistic abstraction results can also be proved likewise, but these follow already by combination with the previous abstraction results.

34

8 Conclusions and Open Problem
In this paper we have presented a variety of congruence, commutativity, and abstraction results that carefully interrelate the reactive, generative, and strati ed models of probabilistic processes. In so doing, we have seen that generative bisimulation ( G ) is not a congruence in the strati ed model, while strati ed bisimulation ( S ) is. However, S is not the largest congruence contained in G (it is too ne). For example, consider P = 1] 1]a : 0 and Q = 1]a : 0. We have ' (P ) 6 S ' (Q) S S G ' (' (C Q])), for any context C ]. yet 'SG ('S (C P ])) SG S It is interesting, therefore, to ask what is the largest congruence contained in G . We can show that, in terms of its distinguishing strength, the following equivalence relation falls strictly between G and S , and is still a congruence in the strati ed model.

De nition 8 An equivalence relation R Pr Pr is a mixed bisimulation if (P; Q) 2 R implies 8S 2 Pr=R,
; S ) = S (Q; ; S ) if both P and Q are probability processes and 8 2 Act; SG (P; ; S ) = SG (Q; ; S )
Two processes P; Q are mixed bisimulation equivalent (written P M Q) if there exists a mixed bisimulation R such that (P; Q) 2 R.
S (P;

Mixed bisimulation essentially allows an -transition in one process to be matched by an transition preceded by a number of probability-1 transitions in the other process (the second clause). At the same time, probability-1 transitions at other places may be signi cant in a product context, and must therefore be taken into account (the rst clause). We close with the following: Conjecture (Full Abstraction) In the strati ed model, M is the largest congruence contained in G .

Acknowledgements: We would like to thank Chris Tofts for his collaboration in vGSST90], from which the current paper evolved, and Kim Larsen and Robin Milner for valuable discussions on models of probabilistic processes. We are also indebted to the anonymous referees for their helpful comments.

References
BBS92]
J. C. M. Baeten, J. A. Bergstra & S. A. Smolka (1992): Axiomatizing proba-

bilistic processes: ACP with generative probabilities. Technical report, Dept. of Math and Computing Science, Technical University of Eindhoven, Eindhoven, The Netherlands. Extended abstract in W. R. Cleaveland, editor: Proceedings of CONCUR '92, LNCS 630, Springer-Verlag, Berlin, pp. 472{485, 1992.

35

processes. In Meyer & Tsailin, editors: Logik at Botik, LNCS 363, Springer-Verlag, Berlin, pp. 26{40. Chr90] I. Christoff (1990): Testing equivalences for probabilistic processes. Technical Report DoCS 90/22, Ph.D. Thesis, Department of Computer Science, Uppsala University, Uppsala, Sweden. See also Testing equivalences and fully abstract models for probabilistic processes. In J. C. M. Baeten & J. W. Klop, editors: Proceedings of CONCUR'90, LNCS 458, Springer-Verlag, Berlin, pp. 126{140, 1990. CSZ92] R. Cleaveland, S. A. Smolka & A. E. Zwarico (1992): Testing preorders for probabilistic processes. In W. Kuich, editor: Proceedings of the 19th ICALP, LNCS 623, Springer-Verlag, Berlin. GJS90] A. Giacalone, C.-C. Jou & S. A. Smolka (1990): Algebraic reasoning for probabilistic concurrent systems. In M. Broy & C.B. Jones, editors: Proceedings Working Conference on Programming Concepts and Methods, IFIP TC 2, Sea of Gallilee, Israel, pp. 443{458. vGSST90] R. J. van Glabbeek, S. A. Smolka, B. Steffen & C. M. N. Tofts (1990): Reactive, generative, and strati ed models of probabilistic processes. In Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science, Philadelphia, PA, pp. 130{141. HJ90] H. Hansson & B. Jonsson (1990): A calculus for communicating systems with time and probabilities. In Proceedings of the 11th IEEE Symposium on Real-Time Systems, Orlando, Florida. JP89] C. Jones & G. D. Plotkin (1989): A probabilistic powerdomain of evaluations. In Proceedings of the 4th Annual IEEE Symposium on Logic in Computer Science. JL91] B. Jonsson & K. G. Larsen (1991): Speci cation and re nement of probabilistic processes. In Proceedings of the 6th Annual IEEE Symposium on Logic in Computer Science, Amsterdam. JS90] C.-C. Jou & S. A. Smolka (1990): Equivalences, congruences, and complete axiomatizations for probabilistic processes. In J. C. M. Baeten & J. W. Klop, editors: Proceedings of CONCUR '90, LNCS 458, Springer-Verlag, Berlin, pp. 367{383. Low91] G. Lowe (1991): Prioritized and probabilistic models of timed CSP. Technical Report PRG-TR-24-91, Oxford University Computing Laboratory, Programming Research Group, 11 Keble Road, Oxford OX1 3QD, England. LS91] K. G. Larsen & A. Skou (1991): Bisimulation through probabilistic testing. Information and Computation 94(1), pp. 1{28. Preliminary report in Proceedings of the 16th Annual ACM Symposium on Principles of Programming Languages, 1989. LS92] K. G. Larsen & A. Skou (1992): Compositional veri cation of probabilistic processes. In W. R. Cleaveland, editor: Proceedings of CONCUR '92, LNCS 630, Springer-Verlag, Berlin, pp. 456{471.

BM89]

B. Bloom & A. R. Meyer (1989): A remark on bisimulation between probabilistic

36

Mil80] Mil83] Mil89] Par81] Plo81] Pnu85] Sei92] SS90] Tof90a] Tof90b] YL92]

R. Milner (1980): A Calculus of Communicating Systems, LNCS 92. Springer-Verlag,

Berlin.

Science 25, pp. 267{310. R. Milner (1989): Communication and Concurrency. International Series in Computer Science. Prentice Hall. D. M. R. Park (1981): Concurrency and automata on in nite sequences. In P. Deussen, editor: Proceedings of the 5th G.I. Conference on Theoretical Computer Science, LNCS 104, Springer-Verlag, Berlin, pp. 167{183. G. D. Plotkin (1981): A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University. A. Pnueli (1985): Linear and branching structures in the semantics and logics of reactive systems. In W. Brauer, editor: Proceedings of the 12th ICALP, Nafplion, LNCS 194, Springer Verlag, Berlin, pp. 15{32. K. Seidel (1992): Probabilistic communicating processes. Technical Report PRG-102, Oxford University Computing Laboratory, Programming Research Group, 11 Keble Road, Oxford OX1 3QD, England. S. A. Smolka & B. U. Steffen (1990): Priority as extremal probability. In J. C. M. Baeten & J. W. Klop, editors: Proceedings of CONCUR '90, LNCS 458, SpringerVerlag, Berlin, pp. 456{466. C. M. N. Tofts (1990): Proof Methods and Pragmatics for Parallel Programming. PhD thesis, LFCS, University of Edinburgh. C. M. N. Tofts (1990): A synchronous calculus of relative frequency. In J. C. M. Baeten & J. W. Klop, editors: Proceedings of CONCUR '90, LNCS 458, SpringerVerlag, Berlin, pp. 467{480. W. Yi & K. G. Larsen (1992): Testing probabilistic and nondeterministic processes. In Proceedings of Protocol Speci cation, Testing and Veri cation XII, pp. 47{61.

R. Milner (1983): Calculi for synchrony and asynchrony. Theoretical Computer

37

ÔÞÖúÉÌÁ´½Ó

¸ü¶àÏà¹ØÎÄÕÂ£º