Reactive, Generative and Stratified Models of Probabilistic Processes

Rob J. van Glabbeek^{∗}

Computer Science Department, Stanford University Stanford, CA 94305-2140, USA

                              rvg@cs.stanford.edu

Scott A. Smolka^{†}

Department of Computer Science, SUNY at Stony Brook Stony Brook, NY 11794-4400, USA

                               sas@cs.sunysb.edu

Bernhard Steffen

Institut für Mathematik und Informatik, Universität Passau 94040 Passau, Germany

                             bus@fmi.uni-passau.de

We introduce three models of probabilistic processes, namely, reactive, generative and stratified. 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 different actions, and the generative model is derivable from the stratified 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.

[figure: P; Q; a[\frac{1}{4}]; a[\frac{3}{4}]; b[1]; a[1]; b[1]; c[1]; a[\frac{1}{6}]; a[\frac{1}{2}]; b[\frac{1}{3}]; a[\frac{1}{2}]; b[\frac{1}{2}]; 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:

P = \frac{1}{4}a + \frac{3}{4}a . (a + b) + b . c Q = \frac{1}{6}a + \frac{1}{2}a . (\frac{1}{2}a + \frac{1}{2}b) + \frac{1}{3}b . c

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 of an a-experiment, P will branch left with probability \frac{1}{4} and right with probability \frac{3}{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 buttons, Q will unlock its a-button with probability \frac{2}{3} and its b-button with probability \frac{1}{3}. In the former case, Q will branch left with probability \frac{1}{4} and right with probability \frac{3}{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 stratified 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 specification of a scheduler for these processes would be

Sc = fix_{X}(\frac{1}{3}a.X + \frac{1}{3}b.X + \frac{1}{3}c.X)

[figure: a; b; c; \frac{1}{3}; \frac{2}{3}; \frac{1}{2}; \frac{1}{2}; a[\frac{1}{3}]; b[\frac{1}{3}]; c[\frac{1}{3}]; a; b; c; X; X; X; X; X; X]

Figure 2: Stratified and generative transition systems of Sc′.

where the action a identifies 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 specification, we would naturally arrive at the expression

fix_{X}(\frac{1}{2}a.X + \frac{1}{2}b.X)

Now, however, the garbage collector is granted one half of the CPU which is different from our original intent. An exact specification of the scheduler can be obtained through the use of nested expressions of probabilistic choice:

Sc′ = fix_{X}(\frac{1}{3}a.X + \frac{2}{3}(\frac{1}{2}b.X + \frac{1}{2}c.X))

which, in the stratified model, yields the leftmost probabilistic labeled transition system of Figure 2. If user c were now denied access we would obtain

fix_{X}(\frac{1}{3}a.X + \frac{2}{3}b.X)

as desired. Thus, in the stratified 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 Sc′ in the generative model is simply the right one of Figure 2. Thus, in the generative model, Sc is (unfortunately) equivalent to Sc′. We shall see that, in a broader sense, the generative model is an abstraction of the stratified model, in which the branching structure of probabilistic choices has been “flattened.”

The extremal case of nested probabilistic choice in the stratified 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 specification 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 flavor of the language.

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 PCCS_{R} 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 define probabilistic bisimulation on generative and stratified 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 PCCS_{R}, 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 stratified model, the reactive model is an abstraction of the generative model, and the nonprobabilistic model is an abstraction of the reactive model. This reflects the stepwise reduction of “observational power”; i.e. starting from the stratified model, we first abstract from the probabilistic branching structure, then from the relative probabilities among different actions, and finally from all probabilities. We proceed as follows:

• We add to the stratified, generative and reactive operational semantics inter-model abstraction rules, which respectively allow the inference of generative probabilistic transitions from stratified 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 define “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 stratified transition systems specified 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 stratified 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 stratified transition systems G and H: G ∼^{S} H ⟹ φ_{SR}(G) ∼^{R} φ_{SR}(H)

Note that our last abstraction result holds for all stratified transition systems and is therefore not directly obtainable from the first two via the φ_{SR} shortcut (which applies only to summation-guarded stratified transition systems).

[figure: φ_{RN}; φ_{GR}; φ_{SG}; φ_{N}; φ_{R}; φ_{G}; φ_{S}; ⟸; ⟸; ⟸; Bisimulation; Stratified; Bisimulation; Generative; Bisimulation; Reactive; Bisimulation; Nonprobabilistic; Model; Stratified; Model; Generative; Model; Reactive; Model; Nonprobabilistic; PCCS]

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) = φ_{SG}(φ_{S}(P)) if P is summation-guarded or restriction-free
φ_{R}(P) = φ_{GR}(φ_{G}(P)) if P is a summation-guarded PCCS_{R} expression
φ_{R}(P) = φ_{SR}(φ_{S}(P)) if P is a PCCS_{R} expression
φ_{N}(P) = φ_{RN}(φ_{R}(P)) if P is a PCCS_{R} expression
φ_{N}(P) = φ_{SN}(φ_{S}(P)) = φ_{GN}(φ_{G}(P))

In the presence of restriction and general summation the first commutativity result does not hold. This is to be expected, as the stratified model is motivated by its different 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 stratified flavor 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 define in a compositional way a more generatively flavored summation in the reactive model, that would allow a generalization of the second commutativity result.

• We then show that the equivalence induced on the stratified (generative) model via abstraction to the generative (reactive) model is not a congruence with respect to PCCS. This demonstrates the need for refining 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])) ≁^{G} φ_{SG}(φ_{S}(C[Q]))

Similarly for the generative-to-reactive and stratified-to-reactive abstractions.

• On the other hand, the equivalence induced on the stratified model via abstraction to the reactive model is a congruence with respect to PCCS_{R}. Likewise, the equivalences induced on the stratified and generative models via abstraction to the nonprobabilistic model are 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 PCCS_{R}. 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 different models are summarized in Figure 3. Here the upper part reflects the commutativity results, the double arrows below reflect the abstraction results, and the dashed arrows indicate the bisimulations that are induced on the stratified, 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 stratified 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 PCCS_{R} was first 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 stratified model and its operational and bisimulation semantics first 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 first 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 stratified 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′ and Q′ such that P′ and Q′ are probabilistically bisimilar.

Christoff [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.

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 ∈ Λ and α, β ∈ 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 define 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 (α, \overline{α}) ↦ 1 and (\overline{α}, α) ↦ 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 first-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:

E ::= 0 | X | α.E | ∑_{i∈I} [p_{i}] E_{i} where p_{i} ∈ (0, 1], ∑_{i∈I} p_{i} = 1 | E×F | E ^{. . . . . .}A | E[f] | fix_{X}E

Intuitively, 0 is the zero process having no transitions, while α . E performs action α with probability 1 and then behaves like E. The expression ∑[p_{i}] E_{i} offers a probabilistic choice among its constituent behaviors E_{i}. E × F represents synchronized product, and the restricted expression E ^{. . . . . .}A can perform actions only from the set A. Finally, E[f] specifies a relabeling of actions, and fix_{X}E defines a recursive process.

A PCCS expression is guarded if in its syntactic tree, every path from a recursion operator fix_{X} 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 stratified models are well-defined. A PCCS expression is restriction-guarded if in its syntactic tree, every path from a recursion operator fix_{X} to an occurrence of the corresponding variable X either passes through an action operator α., or doesn’t pass through a restriction operator. This excludes expressions like fix_{X}(\frac{1}{3}a.X + \frac{1}{3}b.X + \frac{1}{3}X ^{. . . . . .}\{a\}) but permits non-guarded expressions like fix_{X}(X[f] + (a.X)^{. . . . . .}{b}). We write E ∈ PCCS to indicate that E is a restriction-guarded PCCS expression. An expression having no free variables is called a process, and P r is the set of all restriction-guarded PCCS processes.

For this paper, all summation expressions are required to be finite. It will be convenient to assume that all indices used in summation expressions come from a given set I_{0} not containing 0. Also, we write the binary version of process summation as [p] E + [1 − p] F, assuming an index set {1,2}, and often omit the square brackets around the probabilities.

α . E ⟶^{α} E

E_{j} ⟶^{α} E′, j ∈ I  ⟹ ∑_{i∈I} [p_{i}] E_{i} ⟶^{α} E′

E ⟶^{α} E′, F ⟶^{β} F′ ⟹ E × F ⟶^{αβ} E′ × F′
E ⟶^{α} E′, α ∈ A  ⟹ E ^{. . . . . .}A ⟶^{α} E′ ^{. . . . . .}A
E ⟶^{α} E′  ⟹ E[f] ⟶^{f(α)} E′[f]
E{fix_{X}E/X} ⟶^{α} E′ ⟹ fix_{X}E ⟶^{α} E′

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 difference between PCCS and SCCS is the different 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′ or just P ⟶^{α} P′ if P ⟶^{α} P′ can be derived from these rules. We refer to P ⟶^{α} P′ as a transition and its intuitive meaning is that P can perform action α to become P′. The rules of Figure 4 induce a mapping φ_{N} from P r to a domain of nonprobabilistic labeled transition systems.

Definition 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 ∈ 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 defined as a bijective relation between their reachable states, preserving transitions and the initial state. Isomorphic transition systems are conceptually identified. Now φ_{N}(P) for P ∈ P r is defined to be the transition system (S, T, I) with S = P r, I = P and T the set of transitions

{(P, α, P′) | N ⊢ P ⟶^{α} P′}.

Let ^{|}G_{N} be the domain of transition systems (or process graphs). To extend the mapping φ_{N} : P r → ^{|}G_{N} to an interpretation of the open (restriction-guarded) PCCS expressions in ^{|}G_{N}, let PCCS-^{|}G_{N} be the language PCCS to which all transition systems G ∈ ^{|}G_{N} have been added as constants. We introduce an operational rule G ⟶^{α} G_{s} for each initial transition (I, α, s) in each transition system G = (S, T, I). Here G_{s} denotes the transition system with the same states and transitions as G, but with s as the initial state. Let φ′_{N} be the extension of φ_{N} to closed PCCS-^{|}G_{N} expressions. Now let E be an open PCCS expression and ξ a valuation of the free variables of E in ^{|}G_{N}. 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 finally to define φ_{N}(E)(ξ) = φ′_{N}(E^{ξ}).

Note that the extended φ_{N} in particular defines an interpretation of the PCCS operators in |G_{N}, thereby making ^{|}G_{N} into a PCCS-algebra.

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 P r. 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:

Definition 2 The function μ_{N} : (P r × Act × P(P r)) ⟶ {0, 1} is given by: ∀α ∈ Act, ∀P ∈ P r, ∀S ⊆ P r,

μ_{N}(P, α, S) = \{ \begin{matrix}1 & if ∃Q ∈ S with P ⟶^{α} Q \\ 0 & otherwise \end{matrix}

For an equivalence relation R over P r, we write P r/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 defined as follows:

Definition 3 An equivalence relation R ⊆ P r×P r is a nonprobabilistic bisimulation if (P, Q) ∈ R implies: ∀S ∈ P r/R, ∀α ∈ Act,

μ_{N}(P, α, S) = μ_{N}(Q, α, S)

Two processes P, Q ∈ P r are nonprobabilistic bisimulation equivalent (written P ∼^{N} Q) if there exists a nonprobabilistic bisimulation R such that (P, Q) ∈ R. Two open PCCS expressions E, F ∈ PCCS are nonprobabilistic bisimulation equivalent iff they are nonprobabilistic bisimulation equivalent after any substitution of closed terms for their free variables.

This definition can easily be transformed into a definition 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 ∈ PCCS, E ∼^{N} F ⟺ ∀ valuations ξ, φ_{N}(E)(ξ) ∼^{N} φ_{N}(F)(ξ).

Proposition 1 If R_{i} (i ∈ I) is a collection of bisimulations, then also their reflexive and transitive closure (⋃_{i} R_{i})^{∗} is a bisimulation.

Proof: Since each of the relations R_{i} is symmetric, (⋃_{i} R_{i})^{∗} is also symmetric, and hence an equivalence relation. Now suppose (P, Q) ∈ (⋃_{i} R_{i})^{∗}. Then there are P_{j} (j = 0,…, n) for certain n ∈ IN, such that P = P_{o}, Q = P_{n} and (for j = 1,…, n) (P_{j−1}, P_{j}) ∈ R_{k} for certain k ∈ I. Suppose S ∈ P r/(⋃_{i} R_{i})^{∗} and α ∈ Act. Let 1 ≤ j ≤ n and (P_{j−1}, P_{j}) ∈ R_{k}. Since S is the union of a number of equivalence classes T ∈ P r/R_{k} and μ_{N}(P_{j−1}, α, T) = μ_{N}(P_{j}, α, T) for any T ∈ P r/R_{k}, it follows that μ_{N}(P_{j−1}, α, S) = μ_{N}(P_{j}, α, S). This is true for all j = 1,…, n; thus μ_{N}(P, α, S) = μ_{N}(Q, α, S). Hence (⋃_{i} R_{i})^{∗} is a bisimulation. □

Corollary 2 (Equivalence) Bisimulation equivalence is an equivalence relation on P r.

Proof: From the definition of ∼^{N} it follows that on P r we have

∼^{N} = ⋃ { R | R is nonprobabilistic bisimulation }

Thus by Proposition 1, ∼^{N} is itself a bisimulation and hence an equivalence relation. □

It is not difficult to see that a nonprobabilistic bisimulation is just a strong bisimulation [Mil83, Mil89] that happens to be an equivalence relation. Since strong bisimulation equivalence, defined 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 different 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 off 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 ⊆ P r, A ⊆ Act, S ^{. . . . . .}A designates the set {P ^{. . . . . .}A | P ∈ S}.

A PCCS context is defined 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_{[E]_{{fix \atop X}}} (C_{[E]_{¬fix_{X}}}) is the result of substituting E for all occurrences of Ω in C that are (not) in the scope of an operator fix_{X}. 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 ∈ PCCS, C ∈ 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 definition 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 convention that “C ∈ PCCS[ ]^{∗}” should be read as “C ∈ PCCS[ ] such that C[E], C[F] ∈ P r”, it is enough to show that the equivalence (i.e. reflexive, symmetric, and transitive) closure R of R′ = {(C[E], C[F]) | E ∼^{N} F, C ∈ PCCS[ ]^{∗}} is a bisimulation. This can be established by showing that for all (P, Q) ∈ R, S ∈ P r/R and α ∈ Act,

μ_{N}(P, α, S) = μ_{N}(Q, α, S)

We may assume (P, Q) ∈ R′, because the extension to the equivalence closure is straightforward. Thus we have to show that for all E, F ∈ PCCS with E ∼^{N} F,

∀C ∈ PCCS[ ]^{∗}, ∀S ∈ P r/R, ∀α ∈ 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 ∈ PCCS such that E ∼^{N} F, and suppose (1) is established for pairs E′, F′ ∈ 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′ if the transition P ⟶^{α} P′ can be derived by a proof-tree of depth n or less, and define μ_{N}^{n} : (P r × Act × P(P r)) ⟶ {0, 1} by:

μ_{N}^{n}(P, α, S) = \{ \begin{matrix}1 & if ∃Q ∈ S with N ⊢_{n} P ⟶^{α} Q \\ 0 & otherwise \end{matrix}

Now μ_{N}(P, α, S) = lim_{n→∞}μ_{N}^{n}(P, α, S), so we only have to show that for all n ≥ 0,

∀C ∈ PCCS[ ]^{∗}, ∀S ∈ P r/R, ∀α ∈ Act, μ_{N}^{n}(C[E], α, S) ≤ μ_{N}(C[F], α, S)  (2)

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 ∈ P r/R and α ∈ Act,

μ^{n+1}(E, α, S) ≤ μ(F, α, S)  (3)

∼^{N} is contained in the equivalence relation R. Thus S is the disjoint union of one or more T ∈ P r/ ∼^{N}, and it suffices 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 inequality.

Action prefixing: We have to show that for all C ∈ PCCS[ ]^{∗}, S ∈ P r/R and β ∈ Act,

μ^{n+1}(α . C[E], β, S) ≤ μ(α . C[F], β, S)  (4)

For any E ∈ PCCS, μ^{n+1}(α . E, β, S) = μ(α . E, β, S) = \{ \begin{matrix}1 & if α = β and E ∈ S \\ 0 & otherwise \end{matrix}

Thus, if α ≠ β requirement (4) is fulfilled trivially, and if α = β it follows since C[E] and C[F] are in the same equivalence class S′ ∈ P r/R.

Summation: We have to show that for all C_{i} ∈ PCCS[ ]^{∗}, S ∈ P r/R and α ∈ Act,

μ^{n+1}(∑_{i∈I}[p_{i}] C_{i}[E], α, S) ≤ μ(∑_{i∈I}[p_{i}] C_{i}[F], α, S)  (5)

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

LHS = max_{i∈I}(μ^{n}(C_{i}[E], α, S)) ≤^{induction} max_{i∈I}(μ(C_{i}[F], α, S)) = RHS

Product: We have to show that for all C_{i} ∈ PCCS[ ]^{∗} (i = 1, 2), S ∈ P r/R and γ ∈ Act,

μ^{n+1}(C_{1}[E] × C_{2}[E], γ, S) ≤ μ(C_{1}[F] × C_{2}[F], γ, S)  (6)

Since μ^{n+1}(C_{1}[E] × C_{2}[E], γ, S − (P r × P r)) = 0, we may in (6) replace S by S ∩ (P r × P r). By the definition of R we have (P_{1}, P_{2}) ∈ R∧(Q_{1}, Q_{2}) ∈ R ⇒ (P_{1} ×Q_{1}, P_{2} ×Q_{2}) ∈ R. Hence S∩(P r×P r) is the disjoint union of a collection of sets of the form S_{1}×S_{2} with S_{1}, S_{2} ∈ P r/R, and it suffices to prove (6) for such sets S_{1} × S_{2} instead of S ∩ (P r × P r). Moreover we may assume that γ is of the form (α, β), since otherwise μ^{n+1}(C_{1}[E] × C_{2}[E], γ, S) = 0 and we are done. Thus we have to show that for all C_{i} ∈ PCCS[ ]^{∗}, S_{i} ∈ P r/R (i = 1, 2) and α, β ∈ Act,

μ^{n+1}(C_{1}[E] × C_{2}[E], (α, β), S_{1} × S_{2}) ≤ μ(C_{1}[F] × C_{2}[F], (α, β), S_{1} × S_{2})

LHS = μ^{n}(C_{1}[E], α, S_{1}) · μ^{n}(C_{2}[E], β, S_{2}) ≤^{induction} μ(C_{1}[F], α, S_{1}) · μ(C_{2}[F], β, S_{2}) = RHS

Restriction: We have to show that for all C ∈ PCCS[ ]^{∗}, A ⊆ Act, S ∈ P r/R and α ∈ Act,

μ^{n+1}(C[E]^{. . . . . .}A, α, S) ≤ μ(C[F]^{. . . . . .}A, α, S)  (7)

Since μ^{n+1}(C[E]^{. . . . . .}A, α, S − P r^{. . . . . .}A) = 0, we may in (7) replace S by S ∩ (P r^{. . . . . .}A). By the definition of R we have (P_{1}, P_{2}) ∈ R ⇒ (P_{1} ^{. . . . . .}A, P_{2} ^{. . . . . .}A) ∈ R. Hence S ∩ (P r^{. . . . . .}A) is the disjoint union of a collection of sets of the form S′ ^{. . . . . .}A with S′ ∈ P r/R, and it suffices to prove (7) for such sets S′ ^{. . . . . .}A instead of S ∩ (P r^{. . . . . .}A). Moreover we may assume that α ∈ A, since otherwise μ^{n+1}(C[E]^{. . . . . .}A, α, S) = 0 and we are done. Thus we have to show that for all C ∈ PCCS[ ]^{∗}, A ⊆ Act, S′ ∈ P r/R and α ∈ A,

μ^{n+1}(C[E]^{. . . . . .}A, α, S′ ^{. . . . . .}A) ≤ μ(C[F]^{. . . . . .}A, α, S′ ^{. . . . . .}A)

LHS = μ^{n}(C[E], α, S′) ≤^{induction} μ(C[F], α, S′) = RHS

Relabeling: We have to show that for all C ∈ PCCS[ ]^{∗}, f : Act → Act, S ∈ P r/R and β ∈ Act,

μ^{n+1}(C[E][f], β, S) ≤ μ(C[F][f], β, S)  (8)

Since μ^{n+1}(C[E][f], β, S −P r[f]) = 0, we may in (8) replace S by S ∩P r[f]. By the definition of R we have (P_{1}, P_{2}) ∈ R ⇒ (P_{1}[f], P_{2}[f]) ∈ R. Hence S ∩ P r[f] is the disjoint union of a collection of sets of the form S′[f] with S′ ∈ P r/R, and it suffices to prove (8) for such sets S′[f] instead of S ∩ P r[f]. Thus we have to show that for all C ∈ PCCS[ ]^{∗}, f : Act → Act,

S′ ∈ P r/R and β ∈ Act,
μ^{n+1}(C[E][f], β, S′[f]) ≤ μ(C[F][f], β, S′[f])

LHS = max_{f(α)=β}(μ^{n}(C[E], α, S′)) ≤^{induction} max_{f(α)=β}(μ(C[F], α, S′)) = RHS

Recursion: We have to show that for all C ∈ PCCS[ ] with fix_{X}C ∈ PCCS[ ]^{∗}, S ∈ P r/R and

α ∈ Act,

μ^{n+1}(fix_{X}C[E], α, S) ≤ μ(fix_{X}C[F], α, S)

In case X does not occur free in E or F this follows since

LHS = μ^{n}(C[E]{fix_{X}C[E]/X}, α, S) = μ^{n}(C{fix_{X}C/X}[E], α, S) ≤^{induction}

μ(C{fix_{X}C/X}[F], α, S) = μ(C[F]{fix_{X}C[F]/X}, α, S) = RHS

In case X does occur free in E or F we have E{fix_{X}C[F]/X} ∼^{N} F {fix_{X}C[F]/X} by Definition 3, and since these expressions have fewer free variables than E and F it follows that

μ(C\{fix_{X}C/X\}_{[F]_{{fix \atop X}}}[E\{fix_{X}C[F]/X\}], α, S) = μ(C\{fix_{X}C/X\}_{[F]_{{fix \atop X}}}[F \{fix_{X}C[F]/X\}], α, S) (9)

Hence LHS = μ^{n}(C[E]{fix_{X}C[E]/X}, α, S) = μ^{n}(C_{[E]_{¬fix_{X}}}{fix_{X}C/X}[E], α, S) ≤^{induction}

μ(C_{[E]_{¬fix_{X}}}{fix_{X}C/X}[F], α, S) =^{(9)} μ(C[F]{fix_{X}C[F]/X}, α, S) = RHS

This argument is illustrated in Figure 5. □

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 PCCS_{R}, the sublanguage of PCCS with guarded recursion and without relabeling. We begin by presenting the reactive operational semantics for PCCS_{R} that defines a probabilistic transition system for every PCCS_{R} 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 PCCS_{R}.

We restrict ourselves to guarded recursion in order to ensure that the reactive summation operator is well-defined. 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, consider process P = \frac{1}{2}a.X + \frac{1}{2}b.Y. P has a probability-1 a-transition to X and a probability-1 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 defined in the reactive model if an appropriate normalization procedure were

C

X

fix_{X}

Ω

Ω

and a context C with one free occurrence of X,

one hole in the scope of an operator fix_{X} and one hole outside

such a scope E

X

F

X

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

C

fix_{X} fix_{X}

E

X

E

fix_{X}

C

X

fix_{X}

E

X E

X

C

X

fix_{X}

E

X

E

X

\begin{matrix}C[E]\{fix_{X}C[E]/X\} \\ = C_{[E]_{¬fix_{X}}}\{fix_{X}C/X\}[E] \end{matrix}

C

fix_{X} fix_{X}

F

X

E

fix_{X}

C

X

fix_{X}

F

X F

X

C

X

fix_{X}

F

X

F

X

C_{[E]_{¬fix_{X}}}{fix_{X}C/X}[F] =

C\{fix_{X}C/X\}_{[F]_{{fix \atop X}}}[E\{fix_{X}C[F]/X\}]

Figure 5: The last steps in the congruence proof.

applied. Here three normalization procedures come to mind. Let Q = \frac{1}{3}a.X + \frac{1}{3}a.X + \frac{1}{6}b.Y + \frac{1}{6}c.Z and again rename b into a. Now a “syntactic” normalization procedure would yield a probability-\frac{1}{5} a-transition to Y. This is also the solution obtained by abstracting from the generative or stratified 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-\frac{1}{3} a-transition to Y (by counting the number of summands that can do an astep). But then Q and Q′ = \frac{2}{3}a.X + \frac{1}{6}b.Y + \frac{1}{6}c.Z would behave differently after relabeling, and bisimulation equivalence would not be a congruence. Finally a “semantic” normalization procedure would give the a-transition to Y probability \frac{1}{2} (by counting the number of actions that are renamed into a), but here the disadvantage is that first renaming b in a and then c in a yields a different outcome than doing this in the reverse order. Of course, injective relabelings can be added without problem.

A solution to the problem of defining relabeling in the reactive model has recently been found

α.E ^{⊂}⟶^{α[1]}_{0} E

E_{j} ^{⊂}⟶^{α[q]}_{k} E′  ⟹ ∑_{i∈I} [p_{i}] E_{i} ^{⊂}⟶^{α[p_{j}·q/r]}_{j.k} E′  (j ∈ I, r = ∑_{i∈I} {|p_{i} | E_{i} ^{⊂}⟶^{α[s]}_{l} E′′|})

E ^{⊂}⟶^{α[p]}_{i} E′, F ^{⊂}⟶^{β[q]}_{j} F′ ⟹ E × F ^{⊂}⟶^{αβ [p·q]}_{(i,j)} E′ × F′
E ^{⊂}⟶^{α[p]}_{i} E′  ⟹ E ^{. . . . . .}A ^{⊂}⟶^{α[p]}_{i} E′ ^{. . . . . .}A  (α ∈ A)
E{fix_{X}E/X} ^{⊂}⟶^{α[p]}_{i} E′  ⟹ fix_{X}E ^{⊂}⟶^{α[p]}_{i} E′

Figure 6: Reactive operational semantics of PCCS_{R}.

by Larsen and Skou [personal communication]. They propose to equip a relabeling that renames actions a_{1},…, a_{n} into a with a probability distribution that associates a probability p_{i} to each of the a_{i}’s. These probabilities then determine the normalization factor. As such a probabilistic relabeling is meaningless in the generative and stratified models, we will not consider this solution in the present paper.

The same problems encountered in defining 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 sacrificed in the reactive model.

4.1 Reactive Operational Semantics of PCCS_{R}

The reactive operational semantics of PCCS_{R} is given in Figure 6 as a set of inference rules. Reactive transitions are of the form

P ^{⊂}⟶^{α[p]}_{i} P′

meaning that P, with probability p, can perform an α-transition to become P′. The index i is explained just below.

In the second rule, in which {|, |} 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 I_{R} of reactive indices is the smallest set such that 0 ∈ I_{R}, j ∈ I_{0}, k ∈ I_{R} ⇒ j.k ∈ I_{R}, and i, j ∈ I_{R} ⇒ (i, j) ∈ I_{R}. The purpose of the indices is to distinguish different 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 define cumulative probability distributions.) The following example is illustrative:

([\frac{1}{2}]a . 0 + [\frac{1}{2}]a . 0) ^{⊂}⟶^{a[ \frac{1}{2} ]}_{1.0} 0  ([\frac{1}{2}]a . 0 + [\frac{1}{2}]a . 0) ^{⊂}⟶^{a[ \frac{1}{2} ]}_{2.0} 0

As in the nonprobabilistic case, the reactive operational rules collectively define the semantic mapping φ_{R} from P r_{R}, the closed expressions of PCCS_{R}, and even from the open PCCS_{R} expressions, to the domain of reactive probabilistic labeled transition systems.

Definition 4 A reactive (probabilistic) transition system is a triple (S,T,I) with

– S a set of states,

– T ⊆ S × Act × (0, 1] × I_{R} × S a set of transitions, such that

1. ((s, α, p, i, t) ∈ T ∧ (s, β, q, i, r) ∈ T) ⇒ (α = β ∧ p = q ∧ t = r)

2. ∀s ∈ S, ∀α ∈ Act, ∑ {|p | ∃i ∈ I_{R}, t ∈ S : (s, α, p, i, t) ∈ T |} ∈ {0, 1}

– and I ∈ S the initial state.

The first requirement of T says that all outgoing transitions of a given state have different 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 different indices, and f(I) = I′, where I and I′ are the initial states of the two systems. The mapping φ_{R} is defined just as φ_{N} in the previous section. It is not difficult 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 definition, 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 define reactive bisimulation, we first need to define 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:

Definition 5 (Reactive cPDF) μ_{R}: (P r_{R} × Act × P(P r_{R})) ⟶ [0, 1] is the total function given by : ∀α ∈ Act, ∀ P ∈ P r_{R}, ∀ S ⊆ P r_{R},

μ_{R}(P, α, S) = ∑_{i∈I_{R}} {| p_{i} |P ^{⊂}⟶^{α[p_{i}]}_{i} Q and Q ∈ S|}

Reactive bisimulation can now be defined as follows:

Definition 6 ([LS91]) An equivalence relation R ⊆ P r_{R} × P r_{R} is a reactive bisimulation if (P, Q) ∈ R implies : ∀S ∈ P r_{R}/R, ∀α ∈ Act,

μ_{R}(P, α, S) = μ_{R}(Q, α, S)

Two processes P, Q are reactive bisimulation equivalent (written P ∼^{R} Q) if there exists a reactive bisimulation R such that (P, Q) ∈ R.

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 fixed-point iteration technique of [Mil89].

Like strong bisimulation does for SCCS or CCS, reactive bisimulation equivalence provides a compositional semantics for PCCS_{R} that is consistent with the operational semantics defined in the last section. Specifically:

Theorem 4 (Congruence) For E, F ∈ PCCS_{R}, C ∈ PCCS_{R}[ ]: E ∼^{R} F implies C[E] ∼^{R} C[F]

Proof: Following the previous congruence proof, we define R as the equivalence closure of R′ = {(C[E], C[F]) | E ∼^{R} F, C ∈ PCCS_{R}[ ]^{∗}}. The top of a context C ∈ PCCS_{R}[ ] is the part that remains after first removing every subcontext of the form α.E and subsequently every subcontext not containing Ω. Now let PCCS_{R}^{k}[ ] be the set of all PCCS_{R} contexts with at most k nested summation operators in their top. This time we have to show that for all E, F ∈ PCCS_{R} with E ∼^{R} F, and for all k ∈ IN,

∀C ∈ PCCS_{R}^{k}[ ]^{∗}, ∀S ∈ P r_{R}/R, ∀α ∈ Act, μ_{R}(C[E], α, S) = μ_{R}(C[F], α, S)  (10)

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 ∈ PCCS_{R} 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 PCCS_{R}^{l}[ ] for PCCS[ ], except that the function μ_{R}^{n}: (P r_{R} × Act × P(P r_{R})) ⟶ [0, 1] is given by : ∀α ∈ Act, ∀ P ∈ P r_{R}, ∀ S ⊆ P r_{R},

μ_{R}^{n}(P, α, S) = ∑_{i∈I_{R}} {| p_{i} | R ⊢_{n} P ^{⊂}⟶^{α[p_{i}]}_{i} Q and Q ∈ S|}

and every time we invoke the induction hypothesis, we check that it is applied to contexts in PCCS_{R}^{l}[ ]^{∗} only (in the case of recursion this follows by guardedness of PCCS_{R} 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:

LHS = \frac{∑_{i∈I} p_{i} · μ_{R}^{n}(C_{i}[E], α, S)}{∑_{i∈I} \{|p_{i} | μ_{R}(C_{i}[E], α, P r_{R}) ≠ 0|\}} ≤_{(10)}^{induction} \frac{∑_{i∈I} p_{i} · μ_{R}(C_{i}[F], α, S)}{∑_{i∈I} \{|p_{i} | μ_{R}(C_{i}[F], α, P r_{R}) ≠ 0|\}} = RHS

Here (10) may be applied since C_{i} ∈ PCCS_{R}^{l−1}[ ]^{∗}. □

α.E ⟶^{α[1]} _{0} E

E_{j} ⟶^{α[q]} _{k} E′  ⟹ ∑_{i∈I} [p_{i}] E_{i} ⟶^{α[p_{j}·q]}_{j.k} E′ (j ∈ I)

E ⟶^{α[p]} _{i} E′, F ⟶^{β[q]} _{j} F′ ⟹ E × F ⟶^{αβ [p·q]}_{(i,j)} E′ × F′
E ⟶^{α[p]} _{i} E′  ⟹ E ^{. . . . . .}A ⟶^{α[p/r]}_{i} E′ ^{. . . . . .}A  (α ∈ A , r = ν_{G}(E, A))
E ⟶^{α[p]} _{i} E′  ⟹ E[f] ⟶^{f(α)[p]}_{i} E′[f]
E{fix_{X}E/X} ⟶^{α[p]} _{i} E′  ⟹ fix_{X}E ⟶^{α[p]} _{i} E′

Figure 7: Generative operational semantics of PCCS.

5 The Generative Model

In contrast to the reactive model, which is defined only over the sublanguage PCCS_{R} of PCCS, the generative model is defined 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 different 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 I_{G} of generative indices is equal to I_{R}.

With the exception of restriction, all rules are straightforward adaptations of their nonprobabilistic counterparts. The restriction rule defines 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 definition of ν_{G} is given by

ν_{G}(E, A) = ∑_{i∈I_{G}} {| p_{i} | E ⟶^{α[p_{i}]} _{i} E_{i} , α ∈ A|}

Note that under the assumptions E ⟶^{α[p]} _{i} E′ and α ∈ A, ν_{G}(E, A) > 0. As we consider restrictionguarded recursion only, it will follow from the proof of Theorem 5 that ν_{G} is well-defined.

To illustrate the generative operational semantics, consider the expression

E = (a . 0) × ([\frac{1}{3}]b . X + [\frac{1}{3}]c . Y + [\frac{1}{3}]0)

We have:

E ⟶^{(a,b)[ \frac{1}{3} ]}_{(0,1.0)} 0 × X  E ⟶^{(a,c)[ \frac{1}{3} ]}_{(0,2.0)} 0 × Y

As ν_{G}(E, \{(a, b)\}) = \frac{1}{3}, we also have:

E ^{. . . . . .}{(a, b)} ⟶^{(a,b)[1]}_{(0,1.0)} (0 × X)^{. . . . . .}{(a, b)}

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 ν_{G}(E, Act) = \frac{2}{3}, r = \frac{2}{3}, and thus:

E ^{. . . . . .}\{(a, b)\} ⟶^{(a,b)[ \frac{1}{2} ]}_{(0,1.0)} (0 × X)^{. . . . . .}\{(a, b)\}

In fact, deadlock preserving and eliminating restriction operators can be combined in one language by introducing an operator ^{. . . . . .}A for A ⊆ Act ∪ {0}. 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 defined 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

\frac{1}{2}a.0 + \frac{1}{2}0 and fix_{X}(\frac{2}{3}(X[(a, b) → a] × X[(a, b) → b]) + \frac{1}{3}(a, b).X)

for instance has a deadlock probability of \frac{1}{2}. PCCS may be turned into a semistochastic language by replacing the summation operator by a semistochastic variant, which can be expressed in our

language as ( ∑_{i∈I} [p_{i}] E_{i})^{. . . . . .}Act (using our deadlock eliminating restriction operator), and adapting

the definition of restriction-guardedness. In this language there will be no difference between the deadlock preserving and deadlock eliminating restriction operator, and [p] X + [1 − p] 0 ≡ X.

A generative transition system is defined as a reactive transition system, except that the second requirement of T is changed into

∀s ∈ S, ∑ {|p | ∃α ∈ Act, i ∈ I_{G}, t ∈ S : (s, α, p, i, t) ∈ T |} ≤ 1

Also, the semantic mapping φ_{G} from PCCS to the domain of generative transition systems is defined exactly as φ_{N} and φ_{R}.

5.2 Generative Bisimulation

The extension of reactive bisimulation to the generative model is straightforward. The definition of the generative cPDF μ_{G} is the same as Definition 5 except that it is defined over P r and in terms of indexed generative transitions. Likewise, the definition of a generative bisimulation and of ∼^{G} are the same as in Definition 6, except that they are defined over P r and in terms of μ_{G}. Similar to the reactive case, ∼^{G} is substitutive in PCCS.

Theorem 5 (Congruence) For E, F ∈ PCCS, C ∈ PCCS[ ]: E ∼^{G} F implies C[E] ∼^{G} C[F]

Proof: We follow the reactive congruence proof, but this time with PCCS^{k}[ ] the set of PCCS contexts with at most k nested restriction operators in their top, until we have to show, for k ∈ IN,

∀C ∈ PCCS^{k}[ ]^{∗}, ∀S ∈ P r/R, ∀α ∈ 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

∀k < l, ∀C ∈ PCCS^{k}[ ]^{∗}, ∀A ⊆ Act ._{∪} {0}, ν_{G}(C[E], A) = ν_{G}(C[F], A)  (12)

because (restricting w.l.o.g. to the case A ⊆ Act)

ν_{G}(P, A) = ∑_{S∈P r/R^{α∈A}} μ_{G}(P, α, S)

Now the proof of (11) for k = l continues just like the one for ∼^{N}, defining μ_{G}^{n} similar to μ_{R}^{n} and substituting PCCS^{l}[ ] for PCCS[ ], except that the occurrences of max in the cases of summation and relabeling are replaced by ∑ (in the case of summation followed by p_{i}·), and every time we invoke the induction hypothesis, we check that it is applied to contexts in PCCS^{l}[ ]^{∗} 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 = \frac{μ^{n}(C[E], α, S′)}{ν(C[E], A)} ≤_{(12)}^{induction} \frac{μ(C[F], α, S′)}{ν(C[F], A)} = RHS

Here (12) may be applied since C ∈ PCCS^{l−1}[ ]^{∗}. □

∑_{i∈I} [p_{i}] E_{i} ⟼^{p_{j}}_{j} E_{j}  (j ∈ I)
E ⟼^{p}_{i} E′, F ⟼^{q}_{j} F′ ⟹ E × F ⟼^{p·q}_{(i,j)} E′ × F′
E ⟼^{p}_{i} E′, F ⟶^{α} F′ ⟹ E × F ⟼^{p}_{(i,0)} E′ × F
E ⟶^{α} E′, F ⟼^{p}_{i} F′ ⟹ E × F ⟼^{p}_{(0,i)} E × F′
E ⟼^{p}_{i} E′, E′ ⟶^{A}  ⟹ E ^{. . . . . .}A _{⊢}⟶^{p/ν_{S}(E,A)}_{i} E′ ^{. . . . . .}A
E ⟼^{p}_{i} E′  ⟹ E[f] ⟼^{p}_{i} E′[f]
E{fix_{X}E/X} ⟼^{p}_{i} E′ ⟹ fix_{X}E ⟼^{p}_{i} E′

Figure 8: Stratified operational semantics of PCCS.

6 The Stratified Model

The treatments of the nonprobabilistic, reactive and generative models are extended here to the stratified case.

6.1 Stratified Operational Semantics of PCCS

The stratified 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 ⟼^{p}_{i} Q, meaning that P, with probability p, can behave as the process Q. Here i is an index from the set I_{S} = I_{S}^{0} − {0}, where I_{S}^{0} is the smallest set such that 0 ∈ I_{S}^{0}, I_{0} ⊆ I_{S}^{0} and i, j ∈ I_{S}^{0} ⇒ (i, j) ∈ I_{S}^{0}. This separation of action and probability in the stratified 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 stratified 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) first 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 difference in depth of the purely probabilistic branching structures of the argument processes. For example, we do not want (\frac{1}{2} a.0 + \frac{1}{2} b.0) × c.0 to deadlock simply because there does not exist a probability transition in the right hand argument.

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.

The predicate ⟶^{A} for A ⊆ Act is defined by E ⟶^{A} if E = E_{0} ⟼^{p_{1}}_{i_{1}} E_{1} ⟼^{p_{2}}_{i_{2}} ⋯ ⟼^{p_{n}}_{i_{n}} E_{n} ⟶^{α} E′

for certain n ∈ IN and α ∈ A. It is extended to A ⊆ Act ._{∪} {0} by E ⟶^{A._{∪}{0}} iff (E ⟶^{A} ∨E ⟶^{Act} / ). Thus the condition E′ ⟶^{A} in the rule premise requires that derivative E′ of E is capable of performing an action transition from the set A of permitted actions (or, in case 0 ∈ A, deadlocks). The function ν_{S} calculates the stratified normalization factor and is defined by

ν_{S}(E, A) = ∑_{i∈I_{S}} {| p_{i} | E ⟼^{p_{i}}_{i} E_{i} , E_{i} ⟶^{A} |}

As in the generative case, it will follow from the proof of Theorem 6 that ⟶^{A} and ν_{S} are well-defined.

To illustrate the inference rule for restriction, consider the process

P = \frac{1}{3} a.0 + \frac{2}{3} (\frac{1}{2} b.0 + \frac{1}{2} c.0)

In the following, P is placed in some relevant restriction contexts, resulting in the restriction-free processes on the right-hand side.

\begin{aligned}P ^{. . . . . .}\{b, c\} & ≡ & 1 (\frac{1}{2} b.0 + \frac{1}{2} c.0) \\ P ^{. . . . . .}\{a, c\} & ≡ & \frac{1}{3} a.0 + \frac{2}{3} 1 c.0 \\ P ^{. . . . . .}\{c\} & ≡ & 1 (1 c.0) \end{aligned}

Here ≡ denotes isomorphism of the associated labeled transition systems.

The inference rules for action and probability transitions define the semantic mapping φ_{S} from PCCS to the domain of stratified 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 different index, and deadlock states, having no outgoing transitions. Stratified 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 Stratified Bisimulation

Stratified bisimulation is similar to reactive and generative bisimulation in that processes are required to derive stratified bisimulation equivalence classes with equal cumulative probability. However, the separation of probability and action in the stratified operational semantics is reflected in the definition of stratified bisimulation.

To define stratified bisimulation, we need to: (1) define a function that computes the total probability by which a process can behave the same as any process in a set of processes (the technique is analogous to the one in Definition 5, and thus the details are omitted); (2) lift, as in Definition 2, the action relations to sets of derivative processes. The stratified cumulative PDF μ_{S} incorporates both (1) and (2) in an integrated fashion. In particular, μ_{S} is of the form

μ_{S} : (P r × (Act ∪ { ∗ }) × P(P r)) ⟶ [0, 1]

where ∗ is a dummy symbol used to mark probability transitions. That is, for α∈Act, μ_{S}(P, α, S) ∈ { 0, 1 } indicates whether or not P has an α–transition to some process in S. Otherwise, μ_{S}(P, ∗, S) ∈ [0, 1] specifies the total probability by which P may behave the same as any process in S.

Definition 7 An equivalence relation R ⊆ P r × P r is a stratified bisimulation if (P, Q) ∈ R implies ∀S ∈ P r/R, ∀α ∈ Act ∪ {∗},

μ_{S}(P, α, S) = μ_{S}(Q, α, S)

Two processes P, Q are stratified bisimulation equivalent (written P ∼^{S} Q) if there exists a stratified bisimulation R such that (P, Q) ∈ R.

Theorem 6 (Congruence) For E, F ∈ PCCS, C ∈ PCCS[ ]: E ∼^{S} F implies C[E] ∼^{S} C[F]

Proof: By induction on k (as in the generative case) we establish

∀C ∈ PCCS^{k}[ ]^{∗}, ∀S ∈ P r/R, ∀α ∈ Act ∪ {∗}, μ_{S}(C[E], α, S) = μ_{S}(C[F], α, S)  (13)

where R is defined as usual. Suppose (13) holds for k < l. It then follows that

∀k < l, ∀C ∈ PCCS^{k}[ ]^{∗}, ∀A ⊆ Act ._{∪} {0}, C[E] ⟶^{A} iff C[F] ⟶^{A}  (14)

As a consequence we may write S ⟶^{A} for S ∈ P r/R when P ⟶^{A} for an arbitrary representative P ∈ S. Now, if C[E] is not an action process,

ν_{S}(C[E], A) = ∑_{S⟶^{A}} μ_{S}(C[E], ∗, S)

and therefore

∀k < l, ∀C ∈ PCCS^{k}[ ]^{∗}, ∀A ⊆ Act ._{∪} {0}, ν_{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 α ∈ Act proceeds as the congruence proof for ∼^{N}, except that we check that the induction hypothesis is applied to contexts in PCCS^{l}[ ] 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}, defining μ_{S}^{n} similar to μ_{R}^{n}, but with the following modifications.

Action prefixing: The proof of (4) (with β = ∗) trivializes as μ^{n+1}(α . C[E], ∗, S) = 0.

Summation: The proof of (5) is replaced by

μ^{n+1}(∑_{i∈I}[p_{i}] C_{i}[E], ∗, S) = ∑_{i∈I} {|p_{i} | C_{i}[E] ∈ S|} = ∑_{i∈I} {|p_{i} | C_{i}[F] ∈ S|} = μ(∑_{i∈I}[p_{i}] C_{i}[F], ∗, S)

since, for i ∈ I, C_{i}[E] and C_{i}[F] are in the same equivalence class S′ ∈ P r/R.

Product: The proof of (6) (with γ = ∗) is unchanged until “Moreover”. Then we have to show that for all C_{i} ∈ PCCS^{l}[ ]^{∗} and S_{i} ∈ P r/R (i = 1, 2),

μ^{n+1}(C_{1}[E] × C_{2}[E], ∗, S_{1} × S_{2}) ≤ μ(C_{1}[F] × C_{2}[F], ∗, S_{1} × S_{2})  (16)

For this we distinguish 4 cases, depending on whether or not C_{1}[E] and C_{2}[E] are probability processes. If neither of them are, (16) follows since LHS=0. If both of them are, we have

LHS = μ^{n}(C_{1}[E], ∗, S_{1}) · μ^{n}(C_{2}[E], ∗, S_{2}) ≤^{induction} μ(C_{1}[F], ∗, S_{1}) · μ(C_{2}[F], ∗, S_{2}) = RHS

And if just one of them (say C_{1}[E]) is a probability process, (16) follows since

LHS = μ^{n}(C_{1}[E], ∗, S_{1})· ∑_{β∈Act} μ^{n}(C_{2}[E], β, S_{2}) ≤^{induction}μ(C_{1}[F], ∗, S_{1})· ∑_{β∈Act} μ(C_{2}[F], β, S_{2}) = RHS

Restriction: The proof of (7) is unchanged until “Moreover”. Then we have to show that for all C ∈ PCCS^{l}[ ]^{∗}, A ⊆ Act ∪ {0} and S′ ∈ P r/R,

μ^{n+1}(C[E]^{. . . . . .}A, ∗, S′ ^{. . . . . .}A) ≤ μ(C[F]^{. . . . . .}A, ∗, S′ ^{. . . . . .}A)  (17)

Now the proof of (17) proceeds with a case distinction. In case S′ ⟶^{A} / we have LHS=0=RHS.

In case S′ ⟶^{A} it concludes as in the generative case.

Relabeling: This case (with β = ∗) concludes with

LHS = μ^{n}(C[E], ∗, S′) ≤^{induction} μ(C[F], ∗, S′) = RHS □

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 stratified to the generative model in Section 7.2. Subsequently, we give a direct abstraction from the stratified to the reactive model in Section 7.3. Finally, we briefly sketch the simpler abstraction steps leading from probabilistic to nonprobabilistic models.

7.1 The Generative to Reactive Abstraction

Let E, E′ be PCCS expressions. The inter-model abstraction rule IMAR_{GR} is defined by

E ⟶^{α[p]} _{i} E′ ⟹ E ^{⊂}⟶^{α[p/ν_{G}(E,{α})]}_{i} E′

This rule uses the generative normalization function to convert generative probabilities to reactive ones, thereby abstracting away from the relative probabilities between different actions. We can now define φ_{GR}(φ_{G}(P)) as the reactive transition system that can be inferred from P ’s generative transition system via IMAR_{GR}. By the same procedure as described at the end of Section 3.1, φ_{GR} can be extended to a mapping φ_{GR} : ^{|}G_{G} → ^{|}G_{R}.

Write P ∼^{GR} Q if P, Q ∈ P r are reactive bisimulation equivalent with respect to the transitions derivable from G + IMAR_{GR}, i.e. the theory obtained by adding IMAR_{GR} to the rules of Figure 7. The equivalence ∼^{GR} is defined just like ∼^{R} but using the cPDF μ_{GR} instead of μ_{R}. μ_{GR} is defined by

μ_{GR}(P, α, S) = ∑_{i∈I_{R}(=I_{G})} {| p_{i} | G + IMAR_{GR} ⊢ P ^{⊂}⟶^{α[p_{i}]}_{i} Q and Q ∈ S|}

Theorem 7 (Abstraction) Let G, H ∈ ^{|}G_{G}. 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 ∈ P r 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 different, but would involve defining the reactive and generative bisimulation equivalences formally on transition systems.

Let R be a generative bisimulation on P r. We prove that R is also a reactive bisimulation on P r with respect to the transitions derivable from G + IMAR_{GR}. So let (P, Q) ∈ R, S ∈ P r/R and α ∈ Act. Then

ν_{G}(P, {α}) = ∑_{S∈P r/R} μ_{G}(P, α, S) = ∑_{S∈P r/R} μ_{G}(Q, α, S) = ν_{G}(P, {α}), so

μ_{GR}(P, α, S) = \frac{μ_{G}(P, α, S)}{ν_{G}(P, \{α\})} = \frac{μ_{G}(Q, α, S)}{ν_{G}(Q, \{α\})} = μ_{GR}(Q, α, S) □

We will now investigate to what extent φ_{GR} commutes with the semantic mappings φ_{G} and φ_{R}. This turns out to be the case for PCCS_{R} processes in which all summations are of the form ∑_{i∈I} [p_{i}] α_{i} . E_{i}. We say that such an expression is summation-guarded.

Lemma 1 (Soundness and Completeness of IMAR_{GR}) For E, E′ summation-guarded PCCS_{R} expressions, α ∈ Act, p ∈ (0, 1] and i ∈ I_{R},

R ⊢ E ^{⊂}⟶^{α[p]}_{i} E′ ⟺ G + IMAR_{GR} ⊢ E ^{⊂}⟶^{α[p]}_{i} E′

Proof: As in the congruence proofs, we use induction on the depth of derivation trees, and write

R ⊢_{n} E ^{⊂}⟶^{α[p]}_{i} E′ if the transition E ^{⊂}⟶^{α[p]}_{i} E′ can be derived by a proof-tree of depth n. In the similar definition of G + IMAR_{GR} ⊢_{n} we don’t count the single application of IMAR_{GR} though. We distinguish several cases, depending on the topmost operator of E. The case of action prefixing is trivial.

Guarded summation: R ⊢_{2} ∑_{i∈I} [p_{i}] α_{i} . E_{i} ^{⊂}⟶^{α_{j}[q]}_{j} E_{j}

iff j ∈ I and q = p_{j}/ ∑_{k∈I, α_{k}=α_{j}}p_{k} = p_{j}/ν_{G}( ∑_{i∈I} [p_{i}] α_{i} . E_{i}, {α_{j}})

iff G + IMAR_{GR} ⊢_{2} ∑_{i∈I} [p_{i}] α_{i} . E_{i} ^{⊂}⟶^{α_{j}[q]}_{j} E_{j}.

Product: R ⊢_{n+1} E × F ^{⊂}⟶^{(α,β)[r]}_{(i,j)} E′ × F′

iff R ⊢_{n} E ^{⊂}⟶^{α[p]}_{i} E′, F ^{⊂}⟶^{β[q]}_{j} F′ and p · q = r

iff G + IMAR_{GR} ⊢_{n} E ^{⊂}⟶^{α[p]}_{i} E′, F ^{⊂}⟶^{β[q]}_{j} F′ and p · q = r (by induction)

iff G ⊢_{n} E ⟶^{α[p·ν_{G}(E,{α})]}_{i} E′, F ⟶^{β[q·ν_{G}(F,{β})]}_{j} F′ and p · q = r

iff G ⊢_{n+1} E×F ⟶^{(α,β)[r·s]}_{(i,j)} E′×F′ and s = ν_{G}(E, {α}) · ν_{G}(F, {β}) = ν_{G}(E×F, {(α, β)})

iff G + IMAR_{GR} ⊢_{n+1} E × F ^{⊂}⟶^{(α,β)[r]}_{(i,j)} E′ × F′.

Restriction: R ⊢_{n+1} E ^{. . . . . .}A ^{⊂}⟶^{α[p]}_{i} E′ ^{. . . . . .}A

iff R ⊢_{n} E ^{⊂}⟶^{α[p]}_{i} E′ and α ∈ A

iff G + IMAR_{GR} ⊢_{n} E ^{⊂}⟶^{α[p]}_{i} E′ and α ∈ A (by induction)

iff G ⊢_{n} E ⟶^{α[p·ν_{G}(E,{α})]}_{i} E′ and α ∈ A

iff G ⊢_{n+1} E ^{. . . . . .}A ⟶^{α[p·r]}_{i} E′ ^{. . . . . .}A where r = \frac{ν_{G}(E,\{α\})}{ν_{G}(E,A)} = ν_{G}(E ^{. . . . . .}A, \{α\})

iff G + IMAR_{GR} ⊢_{n+1} E ^{. . . . . .}A ^{⊂}⟶^{α[p]}_{i} E′ ^{. . . . . .}A.

Recursion: R ⊢_{n+1} fix_{X}E ^{⊂}⟶^{α[p]}_{i} E′

iff R ⊢_{n} E{fix_{X}E/X} ^{⊂}⟶^{α[p]}_{i} E′

iff G + IMAR_{GR} ⊢_{n} E{fix_{X}E/X} ^{⊂}⟶^{α[p]}_{i} E′ (by induction)

iff G ⊢_{n} E{fix_{X}E/X} ⟶^{α[p·r]}_{i} E′ where r = ν_{G}(E{fix_{X}E/X}, {α}) = ν_{G}(fix_{X}E, {α})

iff G ⊢_{n+1} fix_{X}E ⟶^{α[p·ν_{G}(fix_{X}E,{α})]}_{i} E′

iff G + IMAR_{GR} ⊢_{n+1} fix_{X}E ^{⊂}⟶^{α[p]}_{i} E′. □

As an immediate consequence of Lemma 1 we have:

Theorem 8 (Commutativity) Let P ∈P r_{R} be summation-guarded. Then φ_{GR}(φ_{G}(P))=φ_{R}(P).

Corollary 9 Let P, Q ∈ P r_{R} be summation-guarded. Then P ∼^{G} Q ⇒ P ∼^{R} Q.

Proof: Theorem 7 says that P ∼^{G} Q ⇒ P ∼^{GR} Q for P, Q ∈ P r. Theorem 8 (or Lemma 1) implies μ_{R}(P, α, S) = μ_{GR}(P, α, S) and hence P ∼^{R} Q ⇔ P ∼^{GR} Q for summation-guarded P, Q ∈ P r_{R}. □

Theorem 8 does not hold in the presence of general summation. Consider the process

P = \frac{1}{3}a . X + \frac{2}{3}(\frac{1}{2}a . Y + \frac{1}{2}b . Z)

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 redefined 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 defined 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 refining the bisimulation semantics when moving from the reactive to the generative model. Consider the PCCS processes

P = \frac{1}{3}a . 0 + \frac{2}{3}b . c . 0 Q = \frac{1}{2}a . 0 + \frac{1}{2}b . c . 0

For P,Q we have P ∼^{GR} Q, i.e.

φ_{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}}) = \frac{2}{3} and μ_{GR}(C[Q], a, [c . 0]_{∼^{R}}) = \frac{1}{2}.

A similar counterexample is obtained by placing P and Q in the summation context C = \frac{1}{2}[ ] + \frac{1}{2}b . 0. In this case μ_{GR}(C[P], b, [c . 0]_{∼^{R}}) = \frac{2}{5} and μ_{GR}(C[Q], b, [c . 0]_{∼^{R}}) = \frac{2}{3}.

7.2 The Stratified to Generative Abstraction

Let E, E′ be PCCS expressions. Then IMAR_{SG} is given by

E ⟶^{α} E′ ⟹ E ⟶^{α[1]} _{0} E′

E ⟼^{p}_{i} E′ ⟶^{α[q]} _{j} E′′ ⟹ E ⟶^{α[p·q]}_{i.j} E′′

where i.j (as in the generative case) denotes the concatenation of two indices. Thus the elements of I_{SG}, the set of indices generated by S + IMAR_{SG}, are sequences, and we let |i| denote the length of such a sequence.

Write P ∼^{SG} Q if P, Q ∈ P r are generative bisimulation equivalent with respect to the transitions derivable from G + IMAR_{SG}. The equivalence ∼^{SG} is defined just like ∼^{G}, but using the cPDF μ_{SG} instead of μ_{G}. μ_{SG} is defined by

μ_{SG}(P, α, S) = ∑_{i∈I_{SG}} {| p_{i} | G + IMAR_{SG} ⊢ P ⟶^{α[p_{i}]} _{i} Q and Q ∈ S|}

Theorem 10 (Abstraction) Let G, H ∈ ^{|}G_{S}. 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 ∈ P r, P ∼^{S} Q ⇒ P ∼^{SG} Q.

We now define

μ_{SG}^{n}(P, α, S) = ∑_{i∈I_{SG}} {| p_{i} | S + IMAR_{SG} ⊢ P ⟶^{α[p_{i}]} _{i} Q, Q ∈ S and |i| = n|}

Let R be a stratified bisimulation on P r. We prove that R is also a generative bisimulation on P r with respect to the transitions derivable from S + IMAR_{SG}, i.e. that for (P, Q) ∈ R, S ∈ P r/R and α ∈ Act,

μ_{SG}(P, α, S) = μ_{SG}(Q, α, S)

As μ_{SG}(P, α, S) = ∑_{n∈IN} μ_{SG}^{n}(P, α, S), it suffices to prove this for every μ_{SG}^{n}, which we will do by induction on n.

μ_{SG}^{1}(P, α, S) = μ_{S}(P, α, S) = μ_{S}(Q, α, S) = μ_{SG}^{1}(Q, α, S)

μ_{SG}^{n+1}(P, α, S) = ∑_{i∈I_{S},j∈I_{SG}} {| p_{i}·q_{j} | S+IMAR_{SG} ⊢ P ⟼^{p_{i}}_{i} R⟶^{q_{j}}_{j} Q, R ∈ P r, Q ∈ S and |j| = n|}

= ∑_{R∈P r} μ_{S}(P, ∗, {R}) · μ_{SG}^{n}(R, α, S)

= ∑_{[R]_{R}∈P r/R}μ_{S}(P, ∗, [R]_{R}) · μ_{SG}^{n}(R↙independent of choice of R ∈ [R]_{R} , α, S)

= ∑_{[R]_{R}∈P r/R}μ_{S}(Q, ∗, [R]_{R}) · μ_{SG}^{n}(R, α, S) = μ_{SG}^{n+1}(Q, α, S) □

IMAR_{SG} has the effect of “flattening” 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 stratified transition system via IMAR_{SG}. For example, let P = \frac{1}{3}a . 0 + \frac{2}{3}(\frac{1}{2}b . 0 + \frac{1}{2}c . 0). Then, by IMAR_{SG}

P ⟶^{a[ \frac{1}{3} ]} _{1.0} 0  P ⟶^{b[ \frac{1}{3} ]} _{2.1.0} 0  P ⟶^{c[ \frac{1}{3} ]} _{2.2.0} 0

Except for the transition indices, these are precisely the transitions of P in the generative model.

Lemma 2 (Soundness and Completeness of IMAR_{SG}) There is a surjection f : I_{G} → I_{SG} such that for E, E′ restriction-free PCCS expressions, α ∈ Act, p ∈ (0, 1] and i ∈ I_{G},

G ⊢ E ⟶^{α[p]} _{i} E′ ⟺ S + IMAR_{SG} ⊢ E ⟶^{α[p]} _{f(i)} E′

Moreover G ⊢ E ⟶^{α[p]} _{i} E′, E ⟶^{β[q]} _{j} E′′, i ≠ j ⟹ f(i) ≠ f(j).

Proof: In Lemma 1 f happened to be the identity function and was therefore not mentioned. 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 G′. The inference rules of G′ 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′ : I_{G} → I_{G′} be the function that exhaustively replaces all occurrences of (0, 0) in an index by 0. Then

G ⊢ E ⟶^{α[p]} _{i} E′ ⟺ G′ ⊢ E ⟶^{α[p]} _{f′(i)} E′

Now let G ⊢ E ⟶^{α[p]} _{i} E′, E ⟶^{β[q]} _{j} E′′ and f′(i) = f′(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′ as “limited injectivity” since f′ 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 G′ instead of G and f : I_{G′} → I_{SG}. This function can be chosen bijective.

Recall that I_{S}^{0} = I_{S} ∪ {0} and let I_{SG}^{0} be the largest set of sequences over I_{S}^{0} such that an index (i, j) can only be followed by either 0 or an index (k, l) such that i.k, j.l ∈ I_{SG}^{0}, and an index 0 can only be followed by an index 0. Then I_{SG} = I_{SG}^{0} ∩ (I_{S})^{∗}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 preserved under stratified derivations. Define head : I_{G′} → I_{S}^{0}, tail : I_{G′} → I_{G′} and the partial function • : I_{S}^{0} × I_{G′} → I_{G′} by

head(0) = 0  tail(0) = 0  0 • 0 = 0
head(i.j) = i  tail(i.j) = j  i • j = i.j  (i ∈ I_{0})
head(i, j)=(head(i), head(j)) tail(i, j) = \begin{cases}(tail(i), tail(j)) & if ≠ (0, 0) \\ 0 & otherwise \end{cases} \begin{matrix}(i, j) • (k, l) = (i • k, j • l) \\ (i, j) • 0 = (i • 0, j • 0) \end{matrix}

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 ≠ 0, head(i) ∈ I_{S} and tail(i) is a shorter index than i. Define f : I_{G′} → I_{SG} by

f(i) = \{ \begin{matrix}0 & if i = 0 \\ head(i) . f(tail(i)) & otherwise \end{matrix}

and g : I_{SG} → I_{G′} by

g(i_{0}. · · · .i_{n}) = (i_{0} • (⋯ (i_{n−1} • i_{n}) ⋯))

Note that f transforms pairs of sequences into sequences of pairs. Clearly f(i) ∈ I_{SG} for i ∈ I_{G′} and g(i) ∈ I_{G′} for i ∈ I_{SG}. 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′ establishes the “moreover” part of the lemma.

We now proceed to prove

G′ ⊢ E ⟶^{α[p]} _{i} E′ ⟺ S + IMAR_{SG} ⊢ E ⟶^{α[p]} _{f(i)} E′

by structural induction on i. In case i = 0 (the induction base) E must be summation-free and there is almost no difference between the generative and stratified (=nonprobabilistic) inference rules, and the statement holds. In case i ≠ 0 we again use induction on the depth of derivation trees, albeit modified ones. Here the modification of a G′ derivation tree consists of removing all ancestors of transitions from summation expressions, and the modification 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 IMAR_{SG}. Moreover, the remaining application of IMAR_{SG} doesn’t count. We now use the notation ⊢_{n} to refer to the depth of modified derivations, and prove

G′ ⊢_{n} E ⟶^{α[p]} _{i} E′ ⟺ S + IMAR_{SG} ⊢_{n} E ⟶^{α[p]} _{f(i)} E′

by induction on n. We distinguish several cases, depending on the topmost operator of E. As i ≠ 0 this operator cannot be action prefixing.

Summation: G′ ⊢_{1} ∑_{i∈I} [p_{i}] E_{i} ⟶^{α[p]}_{j.k} E′ iff G′ ⊢ E_{j} ⟶^{α[q]}_{k} E′ and p = p_{j} · q

iff S + IMAR_{SG} ⊢ E_{j} ⟶^{α[q]}_{f(k)} E′ and p = p_{j} · q (by induction (k < j.k))

iff S + IMAR_{SG} ⊢_{1} ∑_{i∈I} [p_{i}] E_{i} ⟶^{α[p]}_{f(j.k)} E′ (since S ⊢_{1} ∑_{i∈I} [p_{i}] E_{i} _{⊢}⟶^{p_{j}}_{j} E_{j}).

Product: In case i ≠ 0 ≠ j: G′ ⊢_{n+1} E × F ⟶^{(α,β)[r]}_{(i,j)} E′′ × F′′

iff G′ ⊢_{n} E ⟶^{α[p]}_{i} E′′, F ⟶^{β[q]}_{j} F′′ and p · q = r

iff S + IMAR_{SG} ⊢_{n} E ⟶^{α[p]}_{f(i)} E′′, F ⟶^{β[q]}_{f(j)} F′′ and p · q = r (by induction)

iff S ⊢_{n} E _{⊢}⟶^{p_{1}}_{head(i)} E′, F _{⊢}⟶^{q_{1}}_{head(j)} F′,

S + IMAR_{SG} ⊢ E′ ⟶^{α[p_{2}]} _{f(tail(i))} E′′, F′ ⟶^{β[q_{2}]} _{f(tail(j))} F′′ and p_{1} · p_{2} · q_{1} · q_{2} = r

iff S ⊢_{n} E _{⊢}⟶^{p_{1}}_{head(i)} E′, F _{⊢}⟶^{q_{1}}_{head(j)} F′,

G′ ⊢ E′ ⟶^{α[p_{2}]} _{tail(i)} E′′, F′ ⟶^{β[q_{2}]} _{tail(j)} F′′ and p_{1} · p_{2} · q_{1} · q_{2} = r (by induction)

iff S ⊢_{n+1} E × F _{⊢}⟶^{r_{1}}_{(head(i),head(j))} E′ × F′,

G′ ⊢ E′ × F′ ⟶^{(α,β)[r_{2}]}_{tail(i,j)} E′′ × F′′ and r_{1} · r_{2} = r

iff S ⊢_{n+1} E × F _{⊢}⟶^{r_{1}}_{head(i,j)} E′ × F′,

S + IMAR_{SG} ⊢ E′ × F′ ⟶^{(α,β)[r_{2}]}_{f(tail(i,j))} E′′ × F′′ and r_{1} · r_{2} = r (by induction)

iff S + IMAR_{SG} ⊢_{n+1} E × F ⟶^{(α,β)[r]}_{f(i,j)} E′′ × F′′.

In case i ≠ 0 = j: G′ ⊢_{n+1} E × F ⟶^{(α,β)[r]}_{(i,0)} E′′ × F′′

iff G′ ⊢_{n} E ⟶^{α[r]}_{i} E′′, F ⟶^{β[1]}_{0} F′′

iff S + IMAR_{SG} ⊢_{n} E ⟶^{α[r]}_{f(i)} E′′, F ⟶^{β[1]}_{0} F′′ (by induction)

iff S ⊢_{n} E _{⊢}⟶^{r_{1}}_{head(i)} E′, F ⟶^{β} F′′,

S + IMAR_{SG} ⊢ E′ ⟶^{α[r_{2}]}_{f(tail(i))} E′′, F ⟶^{β[1]}_{0} F′′ and r_{1} · r_{2} = r

iff S ⊢_{n} E _{⊢}⟶^{r_{1}}_{head(i)} E′, F ⟶^{β} F′′,

G′ ⊢ E′ ⟶^{α[r_{2}]}_{tail(i)} E′′, F ⟶^{β[1]}_{0} F′′ and r_{1} · r_{2} = r (by induction)

iff S ⊢_{n+1} E × F _{⊢}⟶^{r_{1}}_{(head(i),0)} E′ × F,

G′ ⊢ E′ × F ⟶^{(α,β)[r_{2}]}_{tail(i,0)} E′′ × F′′ and r_{1} · r_{2} = r

iff S ⊢_{n+1} E × F _{⊢}⟶^{r_{1}}_{head(i,0)} E′ × F,

S + IMAR_{SG} ⊢ E′ × F ⟶^{(α,β)[r_{2}]}_{f(tail(i,0))} E′′ × F′′ and r_{1} · r_{2} = r (by induction)

iff S + IMAR_{SG} ⊢_{n+1} E × F ⟶^{(α,β)[r]}_{f(i,0)} E′′ × F′′.

The case i = 0 ≠ j is symmetric.

Relabeling: G′ ⊢_{n+1} E[f] ⟶^{α[p]}_{i} E′′[f]

iff G′ ⊢_{n} E ⟶^{β[p]}_{i} E′′ and f(β) = α

iff S + IMAR_{SG} ⊢_{n} E ⟶^{β[p]}_{f(i)} E′′ and f(β) = α (by induction)

iff S ⊢_{n} E ⟼^{p_{1}}_{head(i)} E′, S + IMAR_{SG} ⊢ E′ ⟶^{β[p_{2}]} _{f(tail(i))} E′′, p_{1} · p_{2} = p and f(β) = α

iff S ⊢_{n} E ⟼^{p_{1}}_{head(i)} E′, G′ ⊢ E′ ⟶^{β[p_{2}]} _{tail(i)} E′′, p_{1} · p_{2} = p and f(β) = α (by induction)

iff S ⊢_{n+1} E[f] ⟼^{p_{1}}_{head(i)} E′[f], G′ ⊢ E′[f] ⟶^{α[p_{2}]} _{tail(i)} E′′[f], p_{1} · p_{2} = p

iff S ⊢_{n+1} E[f] ⟼^{p_{1}}_{head(i)} E′[f], S + IMAR_{SG} ⊢ E′[f] ⟶^{α[p_{2}]} _{f(tail(i))} E′′[f], p_{1} · p_{2} = p (ind.)

iff S + IMAR_{SG} ⊢_{n+1} E[f] ⟶^{α[p]}_{f(i)} E′′[f].

Recursion: G′ ⊢_{n+1} fix_{X}E ⟶^{α[p]}_{i} E′′

iff G′ ⊢_{n} E{fix_{X}E/X} ⟶^{α[p]}_{i} E′′

iff S + IMAR_{SG} ⊢_{n} E{fix_{X}E/X} ⟶^{α[p]}_{f(i)} E′′ (by induction)

iff S ⊢_{n} E{fix_{X}E/X} ⟼^{p_{1}}_{head(i)} E′, S+IMAR_{SG} ⊢ E′ ⟶^{α[p_{2}]}_{f(tail(i))} E′′ and p_{1}·p_{2} = p

iff S ⊢_{n+1} fix_{X}E ⟼^{p_{1}}_{head(i)} E′, S + IMAR_{SG} ⊢ E′ ⟶^{α[p_{2}]}_{f(tail(i))} E′′ and p_{1} · p_{2} = p

iff S + IMAR_{SG} ⊢_{n+1} fix_{X}E ⟶^{α[p]}_{f(i)} E′′. □

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

Theorem 11 (Commutativity) Let P ∈ P r be restriction-free. Then φ_{SG}(φ_{S}(P)) = φ_{G}(P).

Corollary 12 Let P, Q ∈ P r 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 ∈ P r. Theorem 11 (or Lemma 2) implies μ_{G}(P, α, S) = μ_{SG}(P, α, S) and hence P ∼^{G} Q ⇔ P ∼^{SG} Q for restriction-free P, Q ∈ P r. □

Theorem 11 does not hold for arbitrary PCCS processes. Consider the process

P = \frac{1}{3}a . 0 + \frac{2}{3}(\frac{1}{2}b . 0 + \frac{1}{2}c . 0)^{. . . . . .}\{a, b\}

φ_{G}(P) is equal to \frac{1}{2}a . 0 + \frac{1}{2}b . 0 while φ_{SG}(φ_{S}(P)) is equal to \frac{1}{3}a . 0 + \frac{2}{3}b . 0. 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 difference between the generative and stratified models. It suffices to extend Lemma 2 to this case.

Lemma 3 Lemma 2 also holds for summation-guarded PCCS expressions.

Proof: It suffices to add the case for restriction to the proof of Lemma 2. Check that the remark concerning the induction base still holds. For the induction step we use that in the stratified model, if E is summation-guarded and E ⟼^{p}_{i} E′, then E′ is an action process. This can be inferred by a straightforward induction on stratified derivations. It follows that ν_{G}(E, A) = ν_{S}(E, A).

Restriction: G′ ⊢_{n+1} E ^{. . . . . .}A ⟶^{α[p]}_{i} E′′ ^{. . . . . .}A

iff G′ ⊢_{n} E ⟶^{α[p·ν_{G}(E,A)]}_{i} E′′ and α ∈ A

iff S + IMAR_{SG} ⊢_{n} E ⟶^{α[p·ν_{G}(E,A)]}_{f(i)} E′′ and α ∈ A (by induction)

iff S ⊢_{n} E _{⊢}⟶^{p·ν_{S}(E,A)}_{head(i)} E′, f(tail(i)) = 0, S ⊢ E′ ⟶^{α} E′′ and α ∈ A

iff S ⊢_{n+1} E ^{. . . . . .}A ⟼^{p}_{head(i)} E′ ^{. . . . . .}A, S + IMAR_{SG} ⊢ E′ ⟶^{α[1]} _{f(tail(i))} E′′ and α ∈ A

iff S + IMAR_{SG} ⊢_{n+1} E ^{. . . . . .}A ⟶^{α[p]}_{f(i)} E′′ ^{. . . . . .}A. □

Finally, we show that the equivalence induced on the stratified model by generative bisimulation is not a congruence for restriction. Consider processes Sc and Sc′ of Section 1 (the scheduler specifications). We have φ_{SG}(φ_{S}(Sc)) ∼^{G} φ_{SG}(φ_{S}(Sc′)) but, as discussed in Section 1,

φ_{SG}(φ_{S}(Sc^{. . . . . .}{a, b})) ≁^{G} φ_{SG}(φ_{S}(Sc′ ^{. . . . . .}{a, b})).

7.3 The Stratified to Reactive Abstraction

Let E, E′ be PCCS expressions. Then IMAR_{SR} is given by

E ⟶^{α} E′ ⟹ E ^{⊂}⟶^{α[1]}_{0} E′

E ⟼^{p}_{i} E′ ^{⊂}⟶^{α[q]}_{j} E′′ ⟹ E ^{⊂}⟶^{α[ \frac{p·q}{ν_{S} (E,\{α\})} ]}_{i.j} E′′

This inter-model abstraction rule defines a mapping φ_{SR} : ^{|}G_{S} → ^{|}G_{R}. Like the composed mapping φ_{GR} ∘ φ_{SG} : ^{|}G_{S} → ^{|}G_{R}, φ_{SR} flattens trees of probability transitions with action transitions at the leaves into a single-level structure, and normalizes the probabilities to yield a reactive transition system. However, whereas φ_{GR} ∘ φ_{SG} first flattens 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 difference between both approaches. But in general the two mappings are different, as will be demonstrated at the end of this section.

Theorem 13 (Abstraction) Let G, H ∈ ^{|}G_{S}. Then G ∼^{S} H ⇒ φ_{SR}(G) ∼^{R} φ_{SR}(H).

Proof: Combine the proofs of Theorems 10 and 7. (It doesn’t suffice to combine just the theorems themselves since φ_{GR} ∘ φ_{SG}(G) ≠ φ_{SR}(G) for an arbitrary stratified transition system G). □

Theorem 14 (Commutativity) Let P ∈ P r_{R}. 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 modifications in the cases for the topmost operator of E.

Summation: p = p_{j} · q/r where r = ∑_{i∈I} {|p_{i} | E_{i} ^{⊂}⟶^{α[s]}_{l} E′′|} = ν_{S}( ∑_{i∈I} [p_{i}] E_{i}, {α}).

Product: In case i ≠ 0 ≠ j: p_{1} · p_{2} · q_{1} · q_{2} = r · ν_{S}(E, {α}) · ν_{S}(F, {β}) = r · ν_{S}(E × F, {(α, β)}) and r_{1} · r_{2} = r · ν_{S}(E × F, {(α, β)}).

In case i ≠ 0 = j: r_{1} · r_{2} = r · ν_{S}(E, {α}) = r · ν_{S}(E × F, {(α, β)}).

Restriction: R′ ⊢_{n+1} E ^{. . . . . .}A ^{⊂}⟶^{α[p]}_{i} E′′ ^{. . . . . .}A

iff R′ ⊢_{n} E ^{⊂}⟶^{α[p]}_{i} E′′ and α ∈ A

iff S + IMAR_{SR} ⊢_{n} E ^{⊂}⟶^{α[p]}_{f(i)} E′′ and α ∈ A (by induction)

iff S ⊢_{n} E ⟼^{p_{1}}_{head(i)} E′, S + IMAR_{SR} ⊢E′ ^{⊂}⟶^{α[p_{2}]}_{f(tail(i))} E′′, p_{1}· p_{2} = p · ν_{S}(E, {α}) and α∈A

iff S ⊢_{n} E ⟼^{p_{1}}_{head(i)} E′, R ⊢E′ ^{⊂}⟶^{α[p_{2}]}_{tail(i)} E′′, p_{1}·p_{2} = p·ν_{S}(E, {α}) and α∈A (induction)

iff S ⊢_{n+1} E ^{. . . . . .}A ⟼^{r_{1}}_{head(i)} E′ ^{. . . . . .}A, R ⊢E′ ^{. . . . . .}A ^{⊂}⟶^{α[p_{2}]}_{tail(i)} E′′ ^{. . . . . .}A and r_{1} · p_{2} = p · \frac{ν_{S}(E,\{α\})}{ν_{S}(E,A)}

iff S ⊢_{n+1} E ^{. . . . . .}A ⟼^{r_{1}}_{head(i)} E′ ^{. . . . . .}A, S+IMAR_{SR}⊢E′ ^{. . . . . .}A ^{⊂}⟶^{α[p_{2}]}_{f(tail(i))} E′′ ^{. . . . . .}A, r_{1}·p_{2} =p·ν_{S}(E ^{. . . . . .}A, {α})

iff S + IMAR_{SR} ⊢_{n+1} E ^{. . . . . .}A ^{⊂}⟶^{α[p]}_{f(i)} E′′ ^{. . . . . .}A.

Relabeling: This case does not apply as E is a PCCS_{R} expression.

Recursion: p_{1} · p_{2} = p · ν_{S}(E{fix_{X}E/X}, {α}) = p · ν_{S}(fix_{X}E, {α}). □

Corollary 15 Let P, Q ∈ P r_{R}. 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 stratified model by reactive bisimulation through φ_{SR} is not a congruence for relabeling. As a consequence, no compositional definition 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 different. It appears that φ_{SR} preserves some of the stratified flavor of nested PCCS summations, which is lost by φ_{GR} ∘ φ_{SG}.

7.4 The Probabilistic to Nonprobabilistic Abstraction

Let E, E′ be PCCS expressions. Then IMAR_{SN} is given by

E ⟼^{p}_{i} E′ ⟶^{α} E′′ ⟹ E ⟶^{α} E′′

Similarly IMAR_{GN} and IMAR_{RN} are given by

E ⟶^{α[p]} _{i} E′ ⟹ E ⟶^{α} E′

E ^{⊂}⟶^{α[p]}_{i} E′ ⟹ E ⟶^{α} E′

These inter-model abstraction rules simply throw away all probabilities. It is comparatively straightforward to establish the remaining commutativity results announced in the introduction.

Theorem 16 (Abstraction) Let G, H ∈ ^{|}G_{R}. Then G ∼^{R} H ⇒ φ_{RN}(G) ∼^{N} φ_{RN}(H).

Proof: Following the idea of the previous abstraction proofs, we show that a reactive bisimulation on P r_{R} is also a nonprobabilistic bisimulation (with respect to the transitions derivable from R + IMAR_{RN}, but by commutativity these are the same as the ones derivable from N). This follows as μ_{N} is completely determined by μ_{R}, namely

μ_{N}(P, α, S) = \{ \begin{matrix}0 & if & μ_{R}(P, α, S) = 0 \\ 1 & if & μ_{R}(P, α, S) > 0 \end{matrix} □

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

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 stratified models of probabilistic processes. In so doing, we have seen that generative bisimulation (∼^{G}) is not a congruence in the stratified model, while stratified bisimulation (∼^{S}) is. However, ∼^{S} is not the largest congruence contained in ∼^{G} (it is too fine). For example, consider P = [1][1]a . 0 and Q = [1]a . 0. We have φ_{S}(P) ≁^{S} φ_{S}(Q) yet φ_{SG}(φ_{S}(C[P])) ∼^{G} φ_{SG}(φ_{S}(C[Q])), for any context C[ ].

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 stratified model.

Definition 8 An equivalence relation R ⊆ P r × P r is a mixed bisimulation if (P, Q) ∈ R implies ∀S ∈ P r/R,

• μ_{S}(P, ∗, S) = μ_{S}(Q, ∗, S) if both P and Q are probability processes

• and ∀α ∈ 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) ∈ R.

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 significant in a product context, and must therefore be taken into account (the first clause). We close with the following:

Conjecture (Full Abstraction) In the stratified 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 probabilistic 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.

[BM89] B. Bloom & A. R. Meyer (1989): A remark on bisimulation between probabilistic 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 stratified 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): Specification and refinement 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 verification of probabilistic processes. In W. R. Cleaveland, editor: Proceedings of CONCUR ’92, LNCS 630, Springer-Verlag, Berlin, pp. 456–471.

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

[Mil83] R. Milner (1983): Calculi for synchrony and asynchrony. Theoretical Computer Science 25, pp. 267–310.

[Mil89] R. Milner (1989): Communication and Concurrency. International Series in Computer Science. Prentice Hall.

[Par81] D. M. R. Park (1981): Concurrency and automata on infinite sequences. In P. Deussen, editor: Proceedings of the 5th G.I. Conference on Theoretical Computer Science, LNCS 104, Springer-Verlag, Berlin, pp. 167–183.

[Plo81] G. D. Plotkin (1981): A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University.

[Pnu85] 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.

[Sei92] K. Seidel (1992): Probabilistic communicating processes. Technical Report PRG-102, Oxford University Computing Laboratory, Programming Research Group, 11 Keble Road, Oxford OX1 3QD, England.

[SS90] 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, Springer-Verlag, Berlin, pp. 456–466.

[Tof90a] C. M. N. Tofts (1990): Proof Methods and Pragmatics for Parallel Programming. PhD thesis, LFCS, University of Edinburgh.

[Tof90b] 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, Springer-Verlag, Berlin, pp. 467–480.

[YL92] W. Yi & K. G. Larsen (1992): Testing probabilistic and nondeterministic processes. In Proceedings of Protocol Specification, Testing and Verification XII, pp. 47–61.