Technical Report Series

Rapporto di Ricerca DAIS-2011-10

Ottobre 2011

M. Bugliesi, L. Gallina, S. Hamadou,

A. Marin, S. Rossi

Interference-sensitive Preorders for MANETs

Interference-sensitive Preorders for MANETs

M. Bugliesi, L. Gallina, S. Hamadou, A. Marin, and S. Rossi

Universita Ca’ Foscari, Venezia (Italy){bugliesi,lgallina,sh,marin,srossi}@dais.unive.it

Abstract. Connectivity and communication interference are two keyaspects in mobile ad-hoc networks (MANETs). We propose a process al-gebraic model targeted at the analysis of both such aspects of MANETs.The framework includes a probabilistic calculus together with analyti-cal techniques based on a probabilistic observational congruence and aninterference-sensitive semantic preorder. The observational congruenceallows us to verify whether two networks exhibit the same probabilisticbehaviour in terms of connectivity. The semantic preorder, in turn, makesit possible to evaluate the interference level of different, behaviourallyequivalent, networks. We show our framework at work on the analy-sis of the well-known Alternating Bit Protocol, contrasting the behavior(and interference level) of the standard implementation of the protocolagainst an alternative implementation that exploits an ideal interferencecancellation scheme on CDMA transmissions.

1 Introduction

Mobile ad-hoc networks (MANETs) are systems of mobile devices communi-cating with each other via wireless links without a pre-established connectivityinfrastructure. Node mobility is unconstrained in such networks: each device ina MANET is free to move autonomously, thereby continuously changing the un-derlying topology. As a result, highly dynamic routing algorithms are required toensure the desired level of connectivity among devices. In addition, given the ab-sence of a central infrastructure to control the flow of communication inside thenetwork, node mobility contributes to greatly increase the level of interferencecaused by distinct, simultaneous, transmissions.

Communication interference is particularly challenging in MANETs due tothe half-duplex nature of wireless channels, which makes it impossible for atransmitter to atomically detect the presence of other, conflicting transmitters onthe same channels. As a consequence, interference between two transmissions isonly possibly detected by receivers located at the intersection of the transmissionranges of two transmitters. While there exist ad hoc protocols that address theseproblems, e.g., CSMA/CA [14], or CDMA/CA [10], interferences remain one ofthe pivotal aspects in the design of MANET systems and protocols.

Drawing on earlier work on the subject (by the last four authors [2, 3], andby others in the literature [7, 8]), in the present paper we introduce a calculusto provide a formal basis for the analysis of connectivity and the evaluation

of interference in MANETs. Like its predecessors [2, 8], our calculus is builtaround nodes, representing the devices of the systems, and locations, identifyingthe position cells across which each device may move inside the network. Nodemobility is unconstrained, and governed by probability distributions as in [2]. In-stead, wireless synchronization is nondeterministic, and controlled by sequentialprocesses inside the nodes: each transmission broadcasts a message at a givenradio frequency and within a given transmission range. Importantly, multiplenodes may simultaneously transmit along the same channel, over overlappingareas: the calculus provides for an explicit representation of the the collisionsthat may occur at those receivers which lie within the transmission range ofdifferent senders.

The semantics of the calculus is inspired by Segala’s probabilistic automata[12] driven by schedulers to resolve the nondeterministic choice among the prob-ability distributions over target states. We define a probabilistic observationalcongruence in the style of [9] to equate networks exhibiting the same connec-tivity behavior. As in [3, 2], and in contrast to [8], the notion of observability isassociated with nodes listening at specific locations in the network, so as to allowa fine grained analysis of connectivity and interference at different areas withina network. We give a coinductive characterization of observational congruencebased on a labelled transition semantics. We also introduce interference-sensitivepreorders over networks to measure the relative interference level of different, butbehaviorally equivalent, networks. As a result, the preorder may be employed tojustify the replacement of components to lower the overall interference level ofa network while preserving its connectivity properties.

We show our framework at work on the analysis of the well-known Alternat-ing Bit Protocol. Specifically, we draw a comparative analysis of the standardimplementation of the protocol and of an alternative implementation that ex-ploits a simple interference cancellation scheme for CDMA transmissions. Theanalysis proves that the two solutions are behaviorally equivalent, but the latteris superior as it guarantees a strictly lower level of interference.

Plan of the paper. Section 2 introduces the calculus and its observational se-mantics. Section 3 defines the LTS semantics and the associated relation oflabelled bisimilarity which coincides with the observational congruence. Section4 develops a technique for for measuring the level of interference. Section 5 con-cludes the paper.

2 The Calculus

The calculus extends the Probabilistic E-BUM calculus introduced in [2], [6] witha new semantics of communication. The peculiarity of the extended calculus isthe non-atomicity of the output and input actions, which we define after [7] tocapture the presence of interference caused by the simultaneous transmissions oftwo (or more) nodes using the same channel in a common transmission area.

Syntax.

2

Networks Processes

M,N ::= 0 Empty network P,Q ::= 0 Inactive process| n[P ]l Node (or device) | in(c, x).P Input| (νc)M Channel restriction | out〈cL,r, w〉.P Output|M1|M2 Parallel composition | [w1 = w2]P,Q Matching

| A〈w〉 Recursion

Table 1: Syntax

C = channels set, d, c ∈ C;Loc = locations set, l, k, h ∈ Loc;N = names set. In particular letters m,n are used for nodes, and for trans-mission radii. Loc ⊆ N;X = variables set (x, y, z);V = values set (X ∪N ∈ V);

Values set includes names, variables and in general, any basic value (integers,booleans, etc.). Letters u, v are used for closed values, and w for open values. Atuple a1, ..., ak of names is represented by a.

The syntax is shown in Table 1. Networks are collections of nodes, devicesrunning in parallel and using channels to communicate messages. N denotesthe set of networks. As usual, 0 denotes the empty network and M1|M2 theparallel composition of two networks. n[P ]l is a network node named n locatedat the physical location l, and executing the process P . In (νc)M the channelc is private with scope in M . We remark that channels are not values, hencethey may not be transmitted: furthermore, given the structure of the syntacticproductions, channels may not be dynamically created and thus (νc)M simplyplays the role of a CCS-style hiding operator1. We write N to denote the set ofnetworks. A context C[·] is a network term with a hole, defined by the grammar:C[·] ::= [·] | [·]|M | M |[·] | (νc)[·] .

Processes are sequential and live within the nodes: 0 is the inactive process;in(c, x).P is ready to listen to a transmission, while out〈cL,r, w〉.P is ready totransmit. In in(c, x).P , the variables in x are bound with scope in P . As tothe output form, the tag r represents the transmission radius of the sender: thechoice of specific transmission ranges may depend on various parameters, andis left to the process running inside the transmitter node. The tag L, in turn,signals the locations from which the transmission will be observed. We remarkthat L is not a set of names, but it is a set of locations. This is due to thefact that one of the main aims of our model is the analysis of protocols formobile ad hoc networks management (as, e.g. ad hoc routing protocols), wheremessages are often addressed to a set of physical locations within the networkarea, rather than to specific devices.The remaining syntactic forms are standard:[w1 = w2]P,Q behaves as P if w1 = w2, and as Q otherwise. A〈w〉 is the process

1 Of course, since channels represent radio frequencies, they may not be hidden inpractice. Indeed, the use of the hiding operator is only meant to specialize the veri-fication method to some specific class of contexts as we will see later.

3

defined via a (possibly recursive) definition A(x)def= P , with |x| = |w| where x

contains all channels and variables that appear free in P .Two further process forms arise as a result of reduction, due to our charac-

terization of communication. In particular, processes that are ready to send orreceive evolve into active senders and receivers:

P,Q ::= . . . As in Table 1| c(x).P Active input| cL,r〈w〉.P Active output

Here, c(x).P is actively receiving a tuple w of (closed) values via channel c andcontinues as P{w/x}, i.e., as P with w substituted for x (where |x| = |w|).Dually, cL,r〈w〉.P is transmitting a tuple of values w via channel c and thencontinues as P. We say that a process P is active if it is in prefix form, with theprefix denoting an active input or output action. Predicate Active(P ) is true

when P is active, and A(M) denotes the network composed of all the activenodes in M , i.e., all nodes n[P ]l in M with P active.

Nodes cannot be created or destroyed, and move autonomously. Node connec-tivity is verified by looking at the physical location and the transmission radiusof the sender: a message broadcast by a node is received only by the nodes thatlie in the area delimited by the transmission radius of the sender. We presupposea function d(·, ·) which takes two locations and returns the distance separatingthem (function d can be simply the euclidean distance between two locations, ora more complex function dealing with potential obstacles).

Each node n is associated with a pair < rn,Jn >, where rn is a non nega-

tive real number denoting the maximum transmission radius that n can use totransmit, while Jn is the transition matrix of a discrete time Markov chain: eachentry Jnlk is the probability that the node n located at l may move to location k.Hence,

∑k∈Loc Jnlk = 1 for all locations l ∈ Loc. Static nodes inside a network

are associated with the identity Markov chain, i.e., the identity matrix Jnll = 1for all l ∈ Loc and Jnlk = 0 for all l 6= k. We denote by µnl the probabilitydistribution associated with node n located at l, that is, the function over Locsuch that µnl (k) = Jnlk, for all k ∈ Loc. We will model the probabilistic evolutionof the network according to these distributions.

Probability distributions for networks. Let n be a node of a network M and l itslocation. We denote by M{n : l′/l} the network obtained by substituting l byl′ inside the node n and by JMKµnl the probability distribution over the set ofnetworks induced by µnl and defined as follows: for each network M ′,

JMKµnl (M ′) =

{µnl (l′) if M ′ = M{n : l′/l}

0 otherwise

Intuitively, JMKµnl (M ′) is the probability that the network M evolves to M ′ dueto the movement of its node n located at l. We say that M ′ is in the supportof JMKµnl (M ′ ∈ spt(JMKµnl )) if JMKµnl (M ′) 6= 0. We write JMK∆ for the Diracdistribution on the network M , namely the probability distribution defined as:

4

JMK∆(M) = 1 and JMK∆(M ′) = 0 for all M ′ such that M ′ 6= M . Finally, we letθ range over {µnl |n is a node and l ∈ Loc} ∪ {∆}.Reduction Semantics. The dynamics of the calculus is specified by the probabilis-

n[[v = v]P,Q]l ≡ n[P ]l (Struct Then)n[[v1 = v2]P,Q]l ≡ n[Q]l v1 6= v2 (Struct Else)

n[A〈v〉]l ≡ n[P{v/x}]l if A(x)def= P ∧ |x| = |v| (Struct Rec)

M ≡ N if M ≡ O and O ≡ N (Struct Trans)M |N ≡ N |M (Struct Par Comm)M |M ′ ≡ N |M ′ ∀M ′ if M ≡ N (Struct Cxt Par)(M |N)|M ′ ≡M |(N |M ′) (Struct Par Assoc)M |0 ≡M (Struct Zero Par)(νc)0 ≡ 0 (Struct Zero Res)(νc)(νd)M ≡ (νd)(νc)M (Struct Res Res)c 6∈ fc(M) implies (νc)(M | N) ≡M | (νc)N (Struct Res Par)

Table 2: Structural Congruence

tic reduction relation (−→), described in Table 3: it takes the form M−→JM ′Kθ,denoting a transition that leaves from M and leads to a probability distribu-tion JM ′Kθ. As usual, reduction relies on structural congruence (≡), the leastcongruence relation satisfying the rules defined in Table 2.

The synchronization over a wireless channels is described by the two rules(R-Bgn-Bcast) and (R-End-Bcast). (R-Bgn-Bcast) models the start of a trans-mission, with node n transiting from ready to active state to transmit messagev on channel c with radius r. The state change in n may cause a collision, whichthe rule captures as follows. The set I is the set of the nodes actively trans-mitting, while the set J is the set of the nodes activly receiving. Finally theset K denotes the nodes ready to begin receiving a message. Given that all thetransmitters are out of n’s range (because d(l, li) ≤ ri), n transits into activestate: this awakes the nodes nk, k ∈ K as they are now in range of an activesender, and at the same time causes a collision at the nodes in J , which alsoare in range, but they were already active on input: as a result, each nj exits itsactive state, receiving the error signal ⊥. All the remaining active receivers thatdo not sense a collision, and are in the range of an active sender may concludethe synchronisation, as described by the (R-End-Bcast) rule.

As we mentioned earlier, the label L signals the set of locations at which thetransmission will be observed. Notice that L does not play a role in a synchro-nization reduction, as messages are broadcast and observable (and received) byany active receiver in range. On the other hand, we use L to fine-tune our notionof observation in the definition of barb, to be discussed shortly.

Rule (R-Move) describes node mobility. A node n located at l and executinga move action will reach a location with a probability described by the distribu-tion µnl that depends on the Markov chain Jn statically associated with n. Weassume that a node can move only if it is not actively involved in any synchro-

5

(R-Bgn-Bcast)∀i ∈ I.d(l, li) > ri ∀i ∈ I ∀k ∈ K.d(li, lk) > ri ∀h ∈ (J ∪K).d(l, lh) ≤ r

n[out〈cL,r, v〉.P ]l |M−→Jn[cL,r〈v〉.P ]l |M ′K∆

where M ≡∏i∈Ini[cLi,ri〈vi〉.Pi]li |

∏j∈Jnj [c(xj).Pj ]lj |

∏k∈Knk[in(c, xk).Pk]lk ,

M ′ ≡∏i∈Ini[cLi,ri〈vi〉.Pi]li |

∏j∈Jnj [Pj{⊥/xj}]lj |

∏j∈Jnk[c(xk).Pk]lk

(R-End-Bcast)∀i ∈ I.d(l, li) ≤ r

n[cL,r〈v〉.P ]l |∏j∈Jni[c(xj).Pj ]lj−→Jn[P ]l |

∏j∈Jnj [Pj{v/xj}]lj K∆

(R-Res)M−→JM ′Kθ

(νc)M−→J(νc)M ′Kθ(R-Move)

Active(P ) = false

n[P ]l−→Jn[P ]lKµnl

(R-Par)M−→JM ′Kθ

M |N−→JM ′|NKθ(R-Struct)

N ≡M M−→JM ′Kθ M ′ ≡ N ′

N−→JN ′Kθ

Table 3: Reduction Semantics

nization: as a result, nodes may move before starting a synchronization (whenthey are in a ready, but not active, state), while they are static during the actualsynchronization. This is a fairly common assumption in wireless networks, and avery reasonable one for all practical situations, in which wireless synchronizationmay be assumed to be orders of magnitude faster than node mobility.

All the remaining rules are standard, but a further remark is in order aboutthe (R-Par) rule and its interaction with the rules that govern synchronization.In fact, such interactions may give rise to inconsistent network configurations.To see that, observe that an application of the (R-Par) rule may cause messagesto be lost by active receivers located within the range of an active sender, evenwhen there is no interference. Similarly, an application of (R-Par) may excludeany set of active sender and/or receiver from a synchronization: in both cases,the network is left in an inconsistent state, with active senders (dually receivers)and no receiver (sender) in range. While it would be possible to rectify theproblem by including conditions to exclude critical pairs for the (R-Par) andsynchronization rules, it is technically more convenient to simply disregard anyundesired reduction. This is achieved in our definition of observational semantics(to be discussed shortly) by resorting to the notion of “admissible scheduler” toguide the dynamics of networks through “well-formed” executions.

Since we are dealing with a probabilistic reduction semantics, which reducesnetworks into probability distributions, we need a way of representing the stepsof each probabilistic evolution of a network. Formally, given a network M , wewrite M−→θN if M−→JM ′Kθ and N is in the support of JM ′Kθ. Following [4], an

execution for M is a (possibly infinite) sequence of steps M−→θ1M1−→θ2M2.... Wewrite ExecM for the set of all possible executions starting from M , last(e) for the

final state of a finite execution e, ej for the prefix execution M−→θ1M1 . . .−→θjMj

of length j of the execution e = M−→θ1M1 · · · −→θjMj−→θj+1Mj+1 · · · , and e↑ for

6

the set of e′ such that e≤prefixe′. We write M−→∗M ′ if there exists a finite exe-

cution e ∈ ExecM such that last(e) = M ′.

Observational Semantics. Following a standard practice, we formalize the ob-servational semantics for our calculus in terms of a notion barb, that providesthe basic unit of observation [9]. As in other calculi for wireless communication,the definition of barb is naturally expressed in terms of message transmission.However, the technical development is more involved, as our calculus presentsboth non-deterministic and probabilistic aspects, where the non-deterministicchoices arise from the possibility for nodes to perform arbitrary movements.

2.1 Observational Semantics

Following a standard practice, we formalize the observational semantics for ourcalculus in terms of a notion barb, that provides the basic unit of observation[9]. As in other calculi for wireless communication, the definition of barb isnaturally expressed in terms of message transmission. However, the technicaldevelopment is more involved, as our calculus presents both non-deterministicand probabilistic aspects, where the non-deterministic choices are among thepossible probability distributions that a network may follow and arise from thepossibility for nodes to perform arbitrary movements. Notice that the fact thata node performs a movement is arbitrary and unpredictable, while the resultinglocation is surely predictable (it depends on the transition matrix).

We denote by behave(M) = {JM ′Kθ | M −→ JM ′Kθ} the set of the possiblebehaviours of M . In order to solve the non-determinism in a network execution,we consider each possible probabilistic transition M −→ JM ′Kθ as arising from ascheduler (see [12]).

Definition 1 (Scheduler). A scheduler is a total function F assigning to afinite execution e a distribution JNKθ ∈ behave(last(e)).

We denote by Sched the set of all schedulers.Given a network M and a scheduler F , we define the set of executions start-

ing from M and driven by F as:

ExecFM = {e = M−→θ1M1−→θ2M2... | ∀j, Mj−1 −→ JM ′jKθj , JM ′jKθj = F (ej−1)and Mj is in the support of JM ′jKθj}.

Formally, given a finite execution e = M−→θ1M1...−→θkMk starting from a net-work M and driven by a scheduler F we define

PFM (e) = JM ′1Kθ1(M1) · ... · JM ′kKθk(Mk)

where ∀j ≤ k, JM ′jKθj = F (ej−1). We define the probability space on the execu-

tions starting from a given network M as follows. Given a scheduler F , σFieldFMis the smallest sigma field on ExecFM that contains the basic cylinders e↑, wheree ∈ ExecFM . The probability measure ProbFM is the unique measure on σFieldFMsuch that ProbFM (e ↑) = PFM (e). Given a measurable set of networks H, we de-note by ExecFM (H) the set of executions starting from M and crossing a state in

7

H. Formally ExecFM (H) = {e ∈ ExecFM | last(ej) ∈ H for some j}. We denotethe probability for a network M to evolve into a network in H, according to thepolicy given by F , as ProbFM (H) = ProbFM (ExecFM (H)).

As we anticipated, we restrict the class of all networks (resp. executions) tothe class of well-formed networks (resp. executions) where, (1) a transmitter,before transiting in active state checks that, locally, the communication channelis not presently busy with other transmissions, and (2) each active receiver in thenetwork is in the transmission cell of exactly one transmitter. In order to restrictthe set of all executions to the set of well-formed executions, we restrict the setof all schedulers to the following set of admissible schedulers. For this purpose,we introduce the auxiliary operator Top(·) over networks. A channel c is at thetop level of a network M , denoted c ∈ Top(M), if M ≡ (νd)(n[P ]l | N) and Pis of the form in(c, x).Q; c(x).Q; out〈cL,r, w〉.Q; or cL,r〈w〉.Q. Also rememberthat A(M) returns a network composed only by its currently active nodes.

Definition 2 (Well-formed network). A network M is well-formed if eitherA(M) ≡ ∅ or A(M) ≡ (νd)

(∏i∈Ini[cLi,ri〈vi〉.Pi]li |

∏j∈J nj [c(xj).Pj ]lj | A(N)

)and the following conditions hold:

– ∀i, i′ ∈ I.d(li, li′) > max(ri, ri′),– ∀j ∈ J.∃!i ∈ I such that d(lj , li) ≤ ri,– c 6∈ Top(A(N)), and N is well-formed.

Definition 3 (Admissible scheduler). A scheduler F is admissible if for allexecutions e and for all networks M in the support of F (e), M is well-formed.

We shall denote the set of admissible schedulers by Sched and, unless otherwisestated, assume that all schedulers are admissible.

The notion of barb introduced below denotes an observable transmissionwith a certain probability according to a fixed scheduler. In our definition, atransmission is observable only if at least one location in the set of the intendedrecipients is able to receive the message.

Definition 4 (Barb). Let M ≡ (νd)(n[cL,r〈v〉.P ]l|M ′), with c /∈ d. We saythat M has a barb on a channel c at locations K(6= ∅), denoted M ↓c@K , if∃K ⊆ L such that d(l, k) 6 r, ∀k ∈ K.

Definition 5 (Probabilistic Barb). We say that a network M has a proba-bilistic barb with probability p on a channel c to the set K of locations, accordingto the scheduler F , written M⇓Fp c@K, if ProbFM ({N |N ↓c@K}) = p.

Intuitively, for a given network M and scheduler F , if M⇓Fp c@K then there isa positive probability that M , driven by F , performs a transmission on channelc and at least one of the intended recipients is able to correctly listen to it.

In the following, we introduce a probabilistic observational congruence, inthe style of [4].

Schedulers constitute an essential feature for modeling communication pro-tocols as they provide freedom in modeling implementation and incomplete

8

knowledge of the system. However, many schedulers could be in fact unreal-istic. Consider for example schedulers giving priority to communication actionsover movements of the nodes. Such schedulers cancel the two states nature of thecommunication channel since the latter remains in the same state until there is nolonger available communication action. Thus, if the network started with a goodchannel then all the messages will be transmitted correctly without enduring anylost. In contrast, if it started with a bad channel, then it will be retransmittingindefinitely the first packet since the channel remains always bad.

Therefore our aim is the definition of a relation allowing us to compare net-works with respect of a given restricted set of schedulers. In order to define anequivalence relation related to a specific set of schedulers, we need a way tobe sure that the set we chose allows the interactions with any possible context.For this reason we are going to define , given a set F of schedulers and a set{M1,M2, ...} of networks, its contextual superset, allowing M1, M2, ... to interactwith any possible context in the model.

Definition 6. Given a set of networks M, and a set F ⊆ Sched of admissibleschedulers we denote as FM the largest subset of Sched, satisfying the followingproperties:∀F ∈ FM,F ∈ F or ∃F ′ ∈ F such that, ∀ context C0[·], ∀e ∈ ExecFC0[O0],

where O0 ≡M0 ∈M:e = C0[O0] −→θ1 C1[O1] −→θ2 C2[O2]... −→θk Ck[Ok],∃e′ ∈ ExecF ′

M0:

e′ = M0 −→θ′1M1 −→θ′2

M2... −→θ′hMh,

such that:

(i) ∀i ∈ [1− h] ∃j ∈ [1− k] such that:1. Mi−1 ≡ Oj−1

2. Mi ≡ Oj3. θ′i = θj

(ii) ∀j ∈ [1− k], if Oj−1 6≡ Oj, ∃i ≤ j such that (i).1, (i).2 and (i).3 hold.

Now we are able to introduce our equivalence relation.

Definition 7. Given a set M of networks, and a set F ∈ Sched of scehdulers,and a relation R over networks:

– Barb preservation. R is barb preserving w.r.t. FM if MRN and M⇓Fp c@Kfor some F ∈ FM implies that there exists F ′ ∈ FM such that N⇓F

′

p c@K.– Reduction closure. R is reduction closed w.r.t. FM if MRN implies that

for all F ∈ FM, there exists F ′ ∈ FM such that for all classes C ∈ N/R,ProbFM (C) = ProbF

′

N (C).– Contextuality. R is contextual if MRN implies that for every context C[·],

it holds that C[M ]RC[N ].

Our probabilistic observational congruence with respect to a restricted set Fof schedulers and to the set M of networks is defined as the largest relation asfollows.

9

(Beg-Out)−

out〈cL,r, v〉.PcL,r−−−→ cL,r〈v〉.P

(End-Out)−

cL,r〈v〉.PcL,r v−−−→ P

(Beg-In)−

in(c, x).Pc−→ c(x).P

(End-In)−

c(x).Pcϑ−→ P{ϑ/x}

(Then)P

η−→ P ′

[v = v]P,Qη−→ P ′

(Else)Q

η−→ Q′ v1 6= v2

[v1 = v2]P,Qη−→ Q′

(Rec)P{v/x} η−→ P ′ A(x)

def= P

A〈v〉 η−→ P ′

Table 4: LTS rules for Processes

Definition 8 (Probabilistic Observational Congruence with respect toF). Given a set F of schedulers and a set M of networks, Probabilistic obser-vational congruence w.r.t. FM, written ∼=FM

p , is the largest symmetric relationover networks which is reduction closed, barb preserving and contextual.

Two networks are related by ∼=FMp if they exhibit the same probabilistic

behaviour (communications) relative to the corresponding sets of intended re-cipients. In the next section we develop a bisimulation-based proof technique for∼=FMp . It provides an efficient method to check whether two networks are related

by ∼=FMp .

3 A bisimulation-based Proof Technique

LTS Semantics. We define a LTS semantics for our calculus, which is built upontwo sets of rules: one for processes and one for networks. Table 4 presents the

LTS rules for processes. Transitions are of the form Pη−→ P ′, where η ranges

over input and output actions, defined as follows:

η ::= c |cϑ |cL,r | cL,rv with ϑ ::= v | ⊥.

Rules (Beg-Out) and (End-Out) model the beginning and the end of anoutput action. Rule (Beg-In) models a process beginning listening to a channelin order to receive a value. Rule (End-In) models either the correct reception ofa message or the reception of a ⊥ due to a collision. All the remaining rules arestandard.

Table 5 presents the LTS rules for networks. The transitions are of the form

Mγ−→ JM ′Kθ, where M is a network, JM ′Kθ is a distribution over networks, and

γ ranges over the following labels:

γ ::= c?@l |c?ϑ@l | cL![l, r] |cL!v[l, r] | c!v@K / R | τ.

10

(Beg-Snd)P

cL,r−−−→ P ′

n[P ]lcL![l,r]−−−−→ Jn[P ′]lK∆

(End-Snd)P

cL,r v−−−→ P ′

n[P ]lcL!v[l,r]−−−−−→ Jn[P ′]lK∆

(Beg-Rcv)P

c−→ P ′

n[P ]lc?@l−−−→ Jn[P ′]lK∆

(End-Rcv)P

cϑ−→ P ′

n[P ]lc?ϑ@l−−−−→ Jn[P ′]lK∆

(Beg-Bcast)M

cL![l,r]−−−−→ JM ′K∆ Nc?@l′−−−→ JN ′K∆ d(l, l′) ≤ r ∧ AsN (c, l) = AsN (c, l′) = ∅

M |N cL![l,r]−−−−→ JM ′|N ′K∆

(Coll-Bcast)M

cL![l,r]−−−−→ JM ′K∆ Nc?⊥@l′−−−−→ JN ′K∆ d(l, l′) ≤ r ∧ AsN (c, l) = ∅

M |N cL![l,r]−−−−→ JM ′|N ′K∆

(End-Bcast)M

cL!v[l,r]−−−−−→ JM ′K∆ Nc?v@l′−−−−→ JN ′K∆ d(l, l′) ≤ r

M |N cL!v[l,r]−−−−−→ JM ′|N ′K∆

(Lose1)M

cL![l,r]−−−−→ JM ′K∆M

τ−→JM ′K∆(Lose2)

McL!v[l,r]−−−−−→ JM ′K∆M

τ−→JM ′K∆

(Move)Active(P ) = false

n[P ]lτ−→ Jn[P ]lKµn

l

(Res)M

γ−→ JM ′Kθ Chan(γ) 6= c

(νc)Mγ−→ J(νc)M ′Kθ

(Obs)M

cL!v[l,r]−−−−−→ JM ′K∆ R = {l′ : d(l, l′) ≤ r ∧ | AsM (c, l′) |= 1} K ⊆ R ∩ L, K 6= ∅M

c!v@K/R−−−−−−→ JM ′K∆

(Par)M

γ−→ JM ′KθM |N γ−→ JM ′|NKθ

Table 5: LTS rules for Networks

We denote by AsM (c, l) the set of active senders of M on channel c reaching

l, i.e., if A(M) ≡ (νd)(∏

i∈Ini[cLi,ri〈vi〉.Pi]li |∏j∈Jnj [c(xj).Pj ]lj | N

)and

c 6∈ Top(N) then AsM (c, l) = {ni : i ∈ I, d(l, li) ≤ ri}.Rules (Beg-Snd) and (End-Snd) model the transmission of a message v

through channel c with radius r to the set L of observers. Transmissions arenon-atomic actions: indeed, since mobile ad-hoc networks are not controlled byany fixed infrastructure, we have to take into account the possibility for nodes tobe not perfectly synchronized with each other. (Beg-Rcv) models the beginningof a message reception, while (End-Rcv) models both the successful receptionof a message or the reception of a failure message (denoted by ⊥) due to aninterference. Rule (Beg-Bcast) models the beginning of a broadcast messagepropagation: all the nodes lying within the transmission cell of the sender maybegin to receive a message (regardless of the fact that they are in L). Rule (Coll-Bcast) models the collision occurred at the location of a receiver lying within

11

the intersection of the transmission area of different nodes transmitting simul-taneously through the same channel. Rule (End-Bcast) models the conclusionof a broadcast message propagation: all the nodes lying within the transmissioncell of the sender will successfully receive a message. Rule (Obs) models theobservability of a transmission: every transmission may be detected (and henceobserved) by any recipient located within the transmission cell of one senderand outside the “interference area”, that is the intersection of the transmissionareas of the active senders of the network. The label c!v@K / R represents thetransmission of the tuple v of messages via c to the subset K of observers in-side the reachable locations R within the transmission cell of the sender. Noticethat collisions are not observable and only a correctly ended transmission maybe observed. Rule (Par) is standard. Rule (Move) models migration of a mobilenode n from a location l to a location k according to the probability distributionµnl , which depends on the Markov chain Jn statically associated with n. Nodescan move only if they are not executing any active action (i.e., nodes cannotmove while transmitting or receiving). Rules (Lose1) and (Lose2) model bothmessage loss and a local activity of the network which an observer is not partyto. As usual, τ -transitions are used to denote non-observable actions. Finally,rule (Res) models the standard channel restriction, where Chan(γ) = c if γ is ofthe form c?@l; c?ϑ@l; cL![l, r]; cL!v[l, r]; or c!v@K / R, and Chan(τ) = ⊥.

The following theorem establishes the relationship between the reductionsemantics and the LTS one, and shows that they model the same behaviours.

Theorem 1 (Harmony). Let M be a network.

1. If M −→ JM ′Kθ then there exist N and N ′ such that Nτ−→ JN ′Kθ, M ≡ N

and M ′ ≡ N ′.2. M ↓c@K iff M is well-formed and N

c!v@K/R−−−−−−→ JN ′K∆ for some R, v, N ≡Mand M ′.

3. If Mτ−→ JM ′Kθ then M −→ JM ′Kθ.

4. If Mc!v@K/R−−−−−−→ JM ′K∆ then M −→ JM ′K∆.

3.1 Probabilistic labelled bisimilarity

Based on the LTS semantics, we define a probabilistic labelled bisimilarity thatis a complete characterisation of our probabilistic observational congruence. It isbuilt upon the following actions:

α ::= c?@l | c?ϑ@l | c!v@K / R | τ.

Again, we write Mα−→θ N if M

α−→ JM ′Kθ and N is in the support of JM ′Kθ.Moreover we write M

α−→ N if Mα−→θ N for some θ. A labelled execution e

of a network M is a finite (or infinite) sequence of steps: Mα1−→θ1 M1

α2−→θ2

M2...αk−−→θk Mk. With abuse of notation, we define ExecM , last(e), ej and

e ↑ as for unlabeled executions. We denote by lbehave(M) the set of all possi-

ble behaviors of M, i.e., lbehave(M) = {(α, JM ′Kθ) | Mα−→ JM ′Kθ}. Labelled

12

executions arise by resolving the non-determinism of both α and JMKθ. As aconsequence, a scheduler2 for the labelled semantics is a function F assigning apair (α, JMKθ) ∈ lbehave(last(e)) with a finite labelled execution e. We denoteby LSched the set of (admissible) schedulers for the LTS semantics. Given a net-work M and a scheduler F , we define ExecFM as the set of all labelled executionsstarting from M and driven by F .

Since we are interested in weak observational equivalences, that abstract overτ -actions, we introduce the notion of weak action.

Definition 9 (Weak Action). The definition of weak action is the following:

• =⇒ is the transitive and reflexive closure ofτ−→.

• c?@k=⇒ denotes =⇒ c?@k−−−→=⇒

• c?ϑ@k=⇒ denotes =⇒ c?ϑ@k−−−−→=⇒

• c!v@K/R=⇒ denotes =⇒ c!v@K/R−−−−−−→=⇒.

We denote byα

=⇒ the weak actionα

=⇒ if α 6= τ , and =⇒ otherwise.Notice that in the definition above the only observable action is the end of a

transmission: indeed, we are not interested in observing input actions, we wantto consider bisimilar networks that perform different inputs, but exactly thesame transmissions any external observer is able to capture.

However, in the probabilistic setting, while considering a computation withobservable content, it is necessary to take account of the actual probability ofthis computation to ensure that weakly bisimilar systems may not only matchone another’s transitions but also perform these transitions with matching prob-abilities.

To achieve this, we denote by ExecFM (α

=⇒, H) the set of executions that,starting from M , according to the scheduler F , lead to a network in the set Hby performing

α=⇒. Moreover, we define the probability of reaching a network in

H from M by performingα

=⇒, according to a scheduler F as ProbFM (α

=⇒, H) =

ProbFM (ExecFM (α

=⇒, H)).

We denote by ExecFM (α

=⇒, H) the set of executions that, starting from M ,

according to the scheduler F , lead to a network in the set H by performingα

=⇒.Moreover, we define ProbFM (

α=⇒, H) = ProbFM (ExecFM (

α=⇒, H)).

Since we want our bisimulation to be a complete characterisation of ournotion of behavioural equivalence, which has been defined with respect to arestricted set of scheduler F ⊆ Sched on Reduction semantics, we have to thecorresponding set of schedulers for LTS.

Definition 10. Given a set of schedulers F ⊆ Sched, we denote as F ⊆ LSchedits correspondent set for the LTS semantic:∀F ∈ LSched, F ∈ F iff ∃F ∈ F such that:

∀O ∈ N , ∀e ∈ ExecFO:

e = Oα1−→θ1 O1...

αk−−→θk Ok

2 We abuse notation and still use F to denote a scheduler for the LTS semantics.

13

∃e′ ∈ ExecFO:

e′ = O −→θ1 O1... −→θk Ok

Definition 11. Given a set of networksM and a set of schedulers F , we defineFM the largest subset of LSched, satisfying the following properties:∀F ∈ FM, F ∈ F or ∃F ′ ∈ F such that, ∀C0[·] and ∀O0 ≡ M0 for some

M0 ∈M:∀e ∈ ExecFC0[O0]:

e = C0[O0]α1−→θ1 C1[O1]...

αk−−→θk Ck[Ok]∃e′ ∈ ExecF ′

M0:

e′ = M0β1−→θ′1

M1...βh−→θ′h

Mh

such that

(i) ∀i ∈ [1− h] ∃j ∈ [1− k] such that

1. Mi−1 ≡ Oj−1

2. Mi ≡ Oj3. θ′i = θj and4. if Cj−1[0] ≡ Cj [0] then βi = αj

otherwise βi = τ or βi = c!v@K / R for some channel c, some messagev and some K ⊆ R sets of locations.

(ii) ∀j ∈ [1 − k] such that Oj−1 6≡ Oj, ∃i ≤ j such that (i).1, (i).2, (i).3, (i).4hold.

Proposition 1.1. Sched{0} = Sched

2. Sched{0} = LSched

Proof. 1. We have that, ∀F ∈ Sched, ∀M0 ∈ N , ∀e ∈ ExecFM0|0:

e = M0 | 0 −→θ1 M1 | 0... −→θk Mk | 0

e′ = 0 ∈ ExecF0 , as required.

2. We have that, ∀F ∈ LSched, ∃F ′ ∈ Sched such that ∀M0 ∈ N , ∀e ∈ExecFM0|0:

e = M0 | 0α1−→θ1 M1 | 0...

αk−−→θk Mk | 0

e′ = 0 ∈ ExecF ′

0 , as required.

Following we will give the definition of probabilistic labelled bisimilarity withrespect to a given set of schedulers. Two conditions are necessary in our defini-tion: the first for output and silent actions and the second for the input ones,since input in our model is not an observable action, hence two systems areconsidered equivalent even if they do not have the same behavior in terms oftransmissions receptions.

14

Definition 12 (Probabilistic Labelled Bisimulation). Let M and N be twonetworks. An equivalence relation R over networks is a probabilistic labelledbisimulation w.r.t. FM if MRN implies: for all scheduler F ∈ FM there existsa scheduler F ′ ∈ FM such that for all α and for all classes C in N/R it holds:

1. if α = τ or α = c!v@K / R then ProbFM (α−→, C) = ProbF

′

N (α

=⇒ C);2. if α = c?@l or α = c?ϑ@l then either ProbFM (

α−→, C) = ProbF′

N (α

=⇒, C) or

ProbFM (α−→, C) = ProbF

′

N (=⇒, C).

Probabilistic labelled bisimilarity, written ≈ ˆFMp , is the largest probabilistic la-

belled bisimulation w.r.t. FM over networks.

4 Interference Metrics

In this section we define a preorder over networks which allows us to comparethe average level of interferences of different networks but exhibiting the sameconnectivity behaviour.

We define two interference metrics. The first one focuses on the senders andcounts how many currently broadcasting nodes might interfere with each otherdue to the overlapping communication ranges. The second metric puts the em-phasis on the receiver nodes and counts the number of active receivers which aresimultaneously reached by two (or more) transmissions.

4.1 Sender-based interference.

Let M be a network. Given a channel c, we denote by Overlaps(M, c) the setof nodes currently broadcasting over c and whose transmission areas are over-lapping at some locations. Formally, let A(M) ≡ (νd)

(∏i∈Ini[cLi,ri〈vi〉.Pi]li |∏

j∈J nj [c(xj).Pj ]lj |M ′)

be the active nodes of M , where c 6∈ Top(M ′), then

Overlaps(M, c) = {ni | i ∈ I, ∃i′(6= i) ∈ I.d(li, li′) ≤ ri + ri′}.

For example, consider the following network

M = n1[out〈cL1,r1 , v1〉.P1]l1 | n2[cL2,r2〈v2〉.P2]l2 | n3[cL3,r3〈v3〉.P3]l3

| n4[aL,r〈v〉.P4]l4 | n5[c(x).P5]l5 | n6[in(c, y).P6]l6

where d(li, li′) > ri for all i, i′ ∈ {1, 2, 3}, i.e., the nodes n1, n2, and n3 are allfar enough away from each other and can broadcast at the same time over thechannel c. In this case, function Overlaps(M, c) is defined as follows: for allc′ 6= c (e.g., c′ = a) Overlaps(M, c′) = ∅, while

Overlaps(M, c) =

{{n2, n3} if d(l2, l3) ≤ r2 + r3

∅ otherwise.

15

We define the sender-based level of interference induced by a probabilisticaction as follows:

Interf s(M,N) =

|Overlaps(N, c)| − |Overlaps(M, c)|

if McL![l,r]−−−−→ JNK∆ for some L, l and r;

0 otherwise.

Consider again the above network M . Since d(l1, li) > r1 for i in {2, 3}, we

have McL1

![l1,r1]−−−−−−→ JNK∆, where

N = n1[cL1,r1〈v1〉.P1]l1 | n2[cL2,r2〈v2〉.P2]l2 | n3[cL3,r3〈v3〉.P3]l3

| n4[aL,r〈v〉.P4]l4 | n5[P ′5]l5 | n6[P ′6]l6

The sender-based level of interference induced by McL1

![l1,r1]−−−−−−→ JNK∆ is, e.g.:

– If n1 is too far away from both n2 and n3, i.e., d(l1, lj) > r1+rj for j in {2, 3},then Overlaps(N , c) = Overlaps(M, c). Hence, Interf s(M, N) = 0.

– If n2 and n3 were already overlapping, i.e., d(l2, l3) ≤ r2+r3 and n1 is not toofar away of at least one of them, i.e., d(l1, l2) ≤ r1 + r2 or d(l1, l3) ≤ r1 + r3

then Overlaps(N , c) = {n1, n2, n3}. Therefore, Interf s(M, N) = 1.

4.2 Receiver-based interference.

We denote by Collr(M, c, l, r) the set of nodes in M which are currentlylistening over channel c and lie in the transmission range of a sender located at lwith radius r. Formally, let A(M) ≡ (νd)

(∏i∈Ini[cLi,ri〈vi〉.Pi]li |

∏j∈J nj [c(xj).Pj ]lj |

M ′)

be the active nodes of M , where c 6∈ Top(M ′), then

Collr(M, c, l, r) = {nj , j ∈ J | d(l, lj) ≤ r}.

The number of receiver-based interferences induced by a probabilistic step is:

Interfr(M,N) =

|Collr(M, c, l, r)| if McL![l,r]−−−−→ JNK∆ for some L;

0 otherwise.

In other words, Interfr(M,N) counts the numbers of listeners in M whichare disturbed by a new begin broadcast action leading to N .

For instance, if we consider again our previous networks M and N , assumingthat n1 can reach both l5 and l6 then P ′5 = P5{⊥/x} and P ′6 = c(y).P6. Then,Collr(M, c, l1, r1) = {n5}. Hence Interfr(M, N) = 1.

Now, let χ ∈ {s, r}. The χ-type number of interferences induced by an exe-cution

e = M0α1−→θ1 M1...

αk−−→θk Mk

is

16

Interfχ(e) =∑ki=1 Interfχ(Mi−1,Mi).

Let H be a set of networks, we denote by PathsFM (H) the set of all execu-tions from M ending in H and driven by F which are not prefix of any otherexecution ending in H. Formally, PathsFM (H) = {e ∈ ExecFM (H) | last(e) ∈H and ∀e′ such that e <prefix e

′, e′ 6∈ PathsFM (H)}. The average number of in-terferences is computed by weighting the number of interferences of each execu-tion by its probability according to F and normalized by the overall probabilityof reaching H.

Definition 13. Let H be a set of networks. The average number of interferencesto reach H from M according to the scheduler F is

InterfχM,F (H) =

∑e∈PathsFM (H) Interfχ(e)× PFM (e)∑

e∈PathsFM (H) PFM (e)

.

Definition 14. Let H be a countable set of sets of networks, and F ⊆ LScheda set of admissible schedulers. We say that N is more interference efficient thanM in the context of H and F , denoted

N vχ〈H,F〉 M,

if N ≈Fp M and, for all scheduler F ∈ F and for all H ∈ H, there exists ascheduler F ′ ∈ F such that InterfχN,F ′(H) ≤ InterfχM,F (H).

5 Related Work

Probabilistic and stochastic models are nowadays widely used in the design andverification of complex systems. In [13] Song and Godskesen propose a proba-bilistic broadcast calculus for mobile and wireless networks whose connectionsare unreliable. Palamidessi et al. in [4] define an extension of the applied pi-calculus with nondeterministic and probabilistic choice operators. Priami [11]introduce a stochastic extension of the pi-caluclus, which allows one to describedynamically reconfigurable or mobile networks. In the context of performanceevaluation, Hillston [5] introduces the process algebra PEPA which is used formodelling systems composed of concurrently active components which co-operateand share work. Bernardo et al. introduce EMPAgr [1], an extended Markovianprocess algebra including probabilities, priority and exponentially distributeddurations. All these calculi abstract from interference, since they consider onlyatomic actions, and they do not allow multiple devices to transmit at the sametime. The problem of interference is considered by Sangiorgi et al. [7] who pro-pose a calculus to detect collisions due to the simultaneous transmissions oftwo or more devices. Differently from our work, their calculus does not supportmobility of nodes and any interference metric is proposed.

17

References

1. M. Bernardo and M. Bravetti. Performance measure sensitive congruences formarkovian process algebras. Theoretical Computer Science, 290(1):117 – 160, 2003.

2. L. Gallina, S. Hamadou, A. Marin, and S. Rossi. A probabilistic energy-awaremodel for mobile ad-hoc networks. In Proc. of the 18th International Conferenceon Analytical and Stochastic Modelling Techniques and Applications (ASMTA’11),volume 6751 of LNCS, pages 316–330. Springer-Verlag, 2011.

3. L. Gallina and S. Rossi. Sender- and receiver-centered interference in wireless adhoc networks. In Proc. of IFIP Wireless Days 2010 (WD’10). IEEE, 2010.

4. J. Goubault-Larrecq, C. Palamidessi, and A. Troina. A probabilistic applied pi-calculus. In Proc. of the 5th Asian Symposium on Programming Languages andSystems (APLAS’07), volume 4807 of LNCS, pages 175–190. Springer-Verlag, 2007.

5. J. Hillston. A Compositional Approach to Performance Modelling. CambridgeUniversity Press, 1996.

6. A. Marin L. Gallina, S. Hamadou and S. Rossi. A framework for throughput andenergy efficiency in mobile ad hoc networks. In Proc. of IFIP Wireless Days 2011.IEEE Press, 2011.

7. I. Lanese and D. Sangiorgi. An operational semantics for a calculus for wirelesssystems. Theoretical Computer Science (TCS’10), 411(19):1928 – 1948, 2010.

8. M. Merro. An observational theory for mobile ad hoc networks. Information andComputation, 207(2):194–208, 2009.

9. R. Milner and D. Sangiorgi. Barbed bisimulation. In Proc. of International Col-loquium on Automata, Languages and Programming (ICALP’92), volume 623 ofLNCS, pages 685–695. Springer-Verlag, 1992.

10. A. Muqattash and M. Krunz. CDMA-based MAC protocol for wireless ad hocnetworks. In Proc. of the 4th ACM International Symposium on Mobile ad hocNetworking & Computing (MobiHoc’03), pages 153–164. ACM, 2003.

11. C. Priami. Stochastic π-calculus. The Computer Journal, 38(7):578–589, 1995.12. R. Segala and N.A. Lynch. Probabilistic simulations for probabilistic processes. In

Proc. of the 5th International Conference on Concurrency Theory (CONCUR’94),volume 836 of LNCS, pages 481–496. Springer-Verlag, 1994.

13. L. Song and J. Godskesen. Probabilistic mobility models for mobile and wirelessnetworks. In Theoretical Computer Science, volume 323 of IFIP Advances in In-formation and Communication Technology, pages 86–100. Springer Boston, 2010.

14. X. Wang and K. Kar. Throughput modelling and fairness issues in CSMA/CAbased ad-hoc networks. In Proc. of the 24th Annual Joint Conf. of the IEEE Com-puter and Communications Societies (INFOCOM’05), pages 23–34. IEEE, 2005.

A Proofs

We start by the proof of the harmony theorem (cf. Theorem 1).

A.1 Harmony [Theorem 1]

We introduce the following auxiliary lemma in order to prove our harmonytheorem.

Lemma 1. Let M be a network.

18

1. If Mc?@l−−−→ JM ′K∆, then exist n, x, a (possibly empty) sequence d such that

c /∈ d, a process P and a (possibly empty) network M1 such that:

M ≡ (νd)(n[in(c, x)P ]l |M1)

andM ′ ≡ (νd)(n[c(x).P ]l|M1).

2. If Mc?ϑ@l−−−−→ JM ′K∆, then exists n, x, d such that c /∈ d and P such that:

M ≡ (νd)(n[c(x).P ]l|M1)

andM ′ ≡ (νd)(n[P{ϑ/x}]l|M1).

3. If McL![l,r]−−−−→ JM ′K∆, then there exist n, v, a (possibly empty) sequence d

such that c /∈ d, a process P , two (possibly empty) sets J and K such that∀h ∈ J ∪K d(l, lh) ≤ r and a (possibly empty) network M1 such that:

M ≡ (νd)(n[out〈cL,r, v〉.P ]l |∏

j∈Jnj [in(c, xj).Pj ]lj |

∏k∈K

nk[c(xk).Pk]lk |M1)

and

M ′ ≡ (νd)(n[cL,r〈v〉.P ]l |∏

j∈Jnj [c(xj).Pj ]lj |

∏k∈K

nK [Pk{⊥/xk}]lk |M1).

4. If McL!v[l,r]−−−−−→ JM ′K∆, then there exist n, a (possibly empty) sequence d such

that c /∈ d, a process P , a (possibly empty) set J , such that ∀j ∈ J d(l, lj) ≤ rand a (possibly empty) network M1 such that:

M ≡ (νd)(n[cL,r〈v〉.P ]l|∏

j∈Jnj [c(xj).Pj ]lj |M1)

andM ≡ (νd)(n[P ]l|

∏j∈J

nj [Pj{v/xj}]lj |M1).

Proof. The proof obtained by induction on the transition rules of Table 5.

Case 1 : Mc?@l−−−→ JM ′K∆

(Beg-Rcv) Let Mc?@l−−−→ JM ′K∆ inferred by rule (Beg-Rcv), then there exist

n, P, l, r such that M ≡ n[P ]l, M′ ≡ n[P ′]l and

P = in(c, x).Q and P ′ = c(x).Q. If we consider the empty network M1 andthe empty sequence d lemma is proved.

(Par) Let M |N c?@l−−−→JM |N ′K∆ inferred by rule (Par), where Mc?@l−−−→JM ′K∆.

By induction hypothesis we have

M ≡ (νd)(n[in(c, x).P ]l|M1)

andM ′ ≡ (νd)(n[c(x).P ]l|M1),

19

for some n, P , x, (possibly empty) d such that c /∈ d, and (possibly empty)M1. By applying rule (Struct Cxt Par), (Struct Par Assoc) and (Struct ResPar) we obtain

M | N ≡ (νd)(n[in(c, x).P ]l|(M1 | N))

andM ′ | N ≡ (νd)(n[in(c, x).P ]l|(M1 | N)).

(Res) Let (νd)Mc?@l−−−→J(νd)M ′K∆ inferred by rule (Res), whereM

c?@l−−−→JM ′K∆and c 6= d. By induction hypothesis we have

M ≡ (νd′)(n[in(c, x).P ]l|M1)

andM ′ ≡ (νd′)(n[c(x).P ]l|M1)

for some n, P , x, (possibly empty) d′ such that c /∈ d′, and (possibly empty)M1.If we consider d′′ = d′ ∪ d, since c /∈ d′′, we get:

(νd)M ≡ (νd′′)(n[in(c, x).P ]l|M1)

and(νd)M ′ ≡ (νd′′)(n[in(c, x).P ]l|M1).

Case 2 : Mc?x@l−−−−→ JM ′K∆

The proof of this case is analogous to the previous one.

Case 3 : McL![l,r]−−−−→ JM ′K∆

(Beg-Snd) Let McL![l,r]−−−−→ JM ′K∆ inferred by rule (Beg-Snd), then ex-

ist v and P such that: M ≡ n[out〈cL,r, v〉.P ]l. Since out〈cL,r, v〉.P¯cL,r−−→

cL,r〈v〉.P , if we suppose d, J , K and M1 empty, lemma is proved because

M ≡ (νd)(n[out〈cL,r, v〉.P ]l|∏j∈J

nj [in(c, xj)Pj ]lj |∏k∈K

nk[c(xk)Pk]lk |M1)

and

M ′ ≡ (νd)(n[cL,r〈v〉.P ]l|∏j∈J

nj [c(xj)Pj ]lj |∏k∈K

nk[Pk{⊥/xk}]lk |M1).

(Beg-Bcast) Let M |N cL![l,r]−−−−→ JM ′|N ′K∆ because McL![l,r]−−−−→ JM ′K∆ and

Nc?@l′−−−→ JN ′K∆, with d(l, l′) ≤ r. By induction hypothesis:

M ≡ (νd1)(n[out〈cL,r, v〉.P ]l|∏j∈J

nj [in(c, xj)Pj ]lj |∏k∈K

nk[c(xk)Pk]lk |M1)

20

and

M ′ ≡ (νd1)(n[cL,r〈v〉.P ]l|∏j∈J

nj [c(xj)Pj ]lj |∏k∈K

nk[Pk{⊥/xk}]lk |M1),

for some n, P , v, l, some (possible empty) sequence d1 such that c /∈ d1,some (possibly empty) sets J and K and some (possibly empty) networkM1, and by indcution hypothesis we get:

N ≡ (νd2)(m[in(c, x).Q]l′ |N1)

andN ′ ≡ (νd2)(m[c(x).Q]l′ |N1),

for some m, Q, x, some (possible empty) sequence d2 such that c /∈ d2 and(possibly empty) network N1 . By applying rules (Struct Cxt Par), (StructPar Assoc) and (Struct Res Par), if we consider d = d1 ∪ d2, we get:

M | N ≡ (νd)(n[out〈cL,r, v〉.P ]l|m[in(c, x).Q]l′ |∏j∈J

nj [in(c, xj)Pj ]lj

|∏k∈K

nk[c(xk)Pk]lk | (M1 | N1))

andM ′ | N ′ ≡ (νd)(n[cL,r〈v〉.P ]l|m[c(x).Q]l′ |

∏j∈J

nj [c(xj)Pj ]lj

|∏k∈K

nk[Pk{⊥/xk}]lk | (M1 | N1)).

(Coll) Let M |N cL![l,r]−−−−→ JM ′|N ′K∆ because McL![l,r]−−−−→ JM ′K∆ and N

c?⊥@l′−−−−→JN ′K∆, with d(l, l′) ≤ r. By induction hypothesis:

M ≡ (νd1)(n[out〈cL,r, v〉.P ]l|∏j∈J

nj [in(c, xj)Pj ]lj |∏k∈K

nk[c(xk)Pk]lk |M1)

and

M ′ ≡ (νd1)(n[cL,r〈v〉.P ]l|∏j∈J

nj [c(xj)Pj ]lj |∏k∈K

nk[Pk{⊥/xk}]lk |M1),

for some n, P , some (possibly empty) sequence d1 such that c /∈ d1, some(possibly empty) sets J and K and some (possibly empty) network M1, andby induction hypothesis we get:

N ≡ (νd2)(m[c(x).Q]l′ |N1)

andN ′ ≡ (νd2)(m[Q{⊥/x}]l′ |N1),

21

for some m, Q, x, some (possibly empty) sequence d2 such that c /∈ d2 and(possibly empty) network N1 . By applying rules (Struct Cxt Par), (StructPar Assoc) and (Struct Res Par), if we consider d = d1 ∪ d2 we get:

M | N ≡ (νd)(n[out〈cL,r, v〉.P ]l|∏j∈J

nj [in(c, xj)Pj ]lj

|∏k∈K

nk[c(xk)Pk]lk | m[c(x).Q]l′ |(M1 | N1))

and

M ′ | N ′ ≡ (νd)(n[cL,r〈v〉.P ]l|∏j∈J

nj [c(xj)Pj ]lj

|∏k∈K

nk[Pk{⊥/xk}]lkm[Q{⊥/x}]l′ | (M1 | N1)).

The proof of the other cases is analogous to the first part of the lemma.

Case 4 : McL!v[l,r]−−−−−→ JM ′K∆

(End-Snd) Let McL!v[l,r]−−−−−→ JM ′K∆ inferred by rule (End-Snd), then exists

P such that M ≡ n[cL,r〈v〉.P ]l. Since cL,r〈v〉.P¯cL,r v−−−→ P , if we suppose J , d

and M1 empty, lemma is proved because

M ≡ (νd)(n[cL,r〈v〉.P ]l|∏j∈J

nj [c(xj)Pj ]lj |M1)

and

M ′ ≡ (νd)(n[P ]l|∏j∈J

nj [Pj{v/xj}]lj |M1).

(End-Bcast) Let M |N cL!v[l,r]−−−−−→ JM ′|N ′K∆ because McL!v[l,r]−−−−−→ JM ′K∆ and

Nc?v@l′−−−−→ JN ′K∆, with d(l, l′) ≤ r. By induction hypothesis:

M ≡ (νd1)(n[cL,r〈v〉.P ]l|∏j∈J

nj [c(xj)Pj ]lj |M1)

and

M ′ ≡ (νd1)(n[P ]l|∏j∈J

nj [Pj{v/xj}]lj |M1),

for some n, P , some (possibly empty) sequence d1 such that c /∈ d1, some(possibly empty) set J and some (possibly empty) network M1, and byinduction hypothesis we get:

N ≡ (νd2)(m[c(x).Q]l′ |N1)

22

andN ′ ≡ (νd2)(m[Q{v/x}]l′ |N1),

for some m, Q, x, some (possibly empty) sequence d2 such that c /∈ d2 and(possibly empty) network N1 . By applying rules (Struct Cxt Par), (StructPar Assoc) and (Struct Res Par), if we consider d = d1 ∪ d2 we get:

M | N ≡ (νd)(n[cL,r〈v〉.P ]l|m[c(x).Q]l′ |∏j∈J

nj [c(xj)Pj ]lj | (M1 | N1))

and

M ′ | N ′ ≡ (νd)(n[P ]l|m[Q{v/x}]l′ |∏j∈J

nj [Pj{v/x}]lj | (M1 | N1)).

The proof of the other cases is analogous to the first part of the lemma.

Lemma 2. If Mγ−→ JM ′Kθ and M ≡ N , then there exists N ′ such that N

γ−→JN ′Kθ and M ′ ≡ N ′.

Proof. By induction on the depth of the inference Mγ−→ JM ′Kθ.

There are a lot of cases to consider, following we give only some example.

(Par) Let consider M | N γ−→ JM ′ | NKθ because Mγ−→ JM ′Kθ. There are several

rules for structural congruence that can be applied.Let consider M | N ≡ M | N ′ because N ′ ≡ N , by (Struct Cxt Par).

By hypothesis Mγ−→ JM ′Kθ and, by an application of rule (Par) we get

M | N ′ γ−→ JM ′ | N ′Kθ. But, since N ′ ≡ N , by applying (Struct Cxt Par) wehave that M ′ | N ′ ≡M ′ | N , as required.Let consider now M | N ≡ N | M by (Struct Par Com). Again, since

Mγ−→ JM ′Kθ, by applying rule (Par) we get N | M γ−→ JN | M ′Kθ, and, by

applying again rule (Struct Par Com), N |M ′ ≡M ′ | N , as required.

(End-Bcast) Let consider M | N cL!v[l,r]−−−−−→ JM ′ | N ′K∆, because McL!v[l,r]−−−−−→ JM ′K∆ and

Nc?v@l′−−−−→ JN ′K∆, and d(l, l′) ≤ r.

Again several rules for structural congruence can be applied.Let consider, e.g. M | N ≡ N | M by (Struct Par Comm). Again, since

McL!v[l,r]−−−−−→ JM ′K∆, N

c?v@l′−−−−→ JN ′K∆, and d(l, l′) ≤ r, we can apply rule

(Bcast), obtaining N | M cL!v[l,r]−−−−−→ JN ′ | M ′K∆, and, by applying again(Struct Par Comm) we get N ′ | M ′ ≡ M ′ | N ′ as required. Let considernow M1 | N ≡M | N because M1 ≡M , by (Struct Cxt Par). By induction

hypothesis M1cL!v[l,r]−−−−−→ JM ′1K∆, and M ′1 ≡ M ′. But since d(l, l′) ≤ r we can

apply rule (Bcast), obtaining M1 | NcL!v[l,r]−−−−−→ JM ′1 | N ′K∆. Now, by applying

(Struct Cxt Par) we get M ′1 | N ′ ≡M ′ | N ′, as required.

The proof of the other cases is similar.

23

Harmony. Now back to the proof of the Theorem 1.

1. The first part is proved by induction on the reduction M −→ JM ′KθSuppose that M −→ JM ′Kθ is due to the application of the rule (R-Move).We simply apply (Move) to obtain:

Active(P ) = false

n[P ]lτ−→ Jn[P ]lKµnl

.

Suppose that M −→ JM ′Kθ is due to the application of the rule (R-Par). Ifwe consider M ≡M1 |M2 and M ′ ≡M ′1 |M2

M1 −→ JM ′1KθM1 |M2 −→ JM ′1 |M2Kθ

,

By induction hypothesis Mτ−→ JM ′Kθ, then by applying rule (Par) we get:

M1τ−→ JM ′1Kθ

M1 |M2τ−→ JM ′1 |M2Kθ

.

Suppose that M −→ JM ′Kθ is due to the application of the rule (R-Res). Ifwe consider M ≡ (νc)M1 and M ′ ≡ (νc)M ′1:

M1 −→ JM ′1Kθ(νc)M1 −→ J(νc)M ′1Kθ

,

by induction hypothesis Mτ−→ JM ′Kθ, then by applying rule (Res), since

Chan(τ) 6= c we get:

M1τ−→ JM ′1Kθ

(νc)M1τ−→ J(νc)M ′1Kθ

.

Suppose that M −→ JM ′Kθ is due to the application of the rule (R-Bgn-Bcast). It means:M ≡ (νd)(n[out〈cL,r, v〉.P ]l |

∏i∈In[cLi,ri〈vi〉.Pi]li

|∏j∈Jn[c(xj).Pj ]lj |

∏k∈Kn[in(c, xk).Pk]lk)

andM ′ ≡ (νd)(n[cL,r〈v〉.P ]l |

∏i∈In[cLi,ri〈vi〉.Pi]li

|∏j∈Jn[Pj{⊥/xj}]lj |

∏k∈Kn[c(xk).Pk]lk).

Then, by applying rule (Beg-Snd), (Beg-Rcv), and then | K | times rule(Beg-Bcast), | J | times rule (Coll-Bcast), and, finally rules (Res), (Lose1)and (Par), we obtain:

Mτ−→≡ J(νd)(n[cL,r〈v〉.P ]l |

∏i∈In[cLi,ri〈vi〉.Pi]li |

∏j∈Jn[Pj{⊥/xj}]lj |∏

k∈Kn[c(xk).Pk]lk)Kθas required.

24

Suppose that M −→ JM ′Kθ is due to the application of the rule (R-End-Bcast). It means:

∀i ∈ I.d(l, li) ≤ rn[cL,r〈v〉.P ]l |

∏j∈Jnj [c(xj).Pj ]lj−→Jn[P ]l |

∏j∈Jnj [Pj{v/xj}]lj K∆

.

Then, by applying rule (End-Snd), (End-Rcv), | I | times rule (End-Bcast)and, finally rule (Lose2), we get:

n[cL,r〈v〉.P ]l |∏

j∈Jnj [c(xj).Pj ]lj

τ−→Jn[P ]l |∏

j∈Jnj [Pj{v/xj}]lj K∆

as required.Finally let suppose that the reduction M −→ JM ′Kθ is due to an applicationof rule (R-Struct):

M ≡ N N−→JN ′Kθ N ′ ≡M ′

M−→JM ′Kθ.

By induction hypothesis there exists N1 ≡ N and N2 ≡ N ′ such that N1τ−→

JN2Kθ. Then, by applying the rule for structural congruence (Struct Trans)we get M ≡ N ≡ N1 and M ′ ≡ N ′ ≡ N2, as required.

2. The second part of the theorem follows from Lemma 1 and the definition ofBarb. If M ↓c@K , by the definition of Barb there exists v, L, r, a (possiblyempty) sequence d such that c 6∈ d, a process P , a (possibly empty) networkM1 such that:M ≡ (νd)(n[cL,r〈v〉.P ]l |M1), with K ⊆ {k ∈ L s.t. d(l, k) ≤ r} and K 6= ∅.By applying the rules (End-Snd) and (Par) we obtain:

n[cL,r〈v〉.P ]lcL!v[l,r]−−−−−→ Jn[P ]lK∆

n[cL,r〈v〉.P ]l |M1cL!v[l,r]−−−−−→ Jn[P ]l |M1K∆

;

then, since K ⊆ R ∩ L and K 6= ∅, we can apply rule (Obs):

n[cL,r〈v〉.P ]l |M1c!v@K/R−−−−−−→ Jn[P ]l |M1K∆,

where R = {l′ ∈ Loc : d(l, l′) ≤ r}, as required.

If Mc!v@K/R−−−−−−→ JM ′K∆, because M

cL!v[l,r]−−−−−→ JM ′K∆, by applying Lemma1 then there exist n, a (possibly empty) sequence d such that c /∈ d, P , a(possibly empty) network M1 and a (possibly empty) set J , such that ∀j ∈ Jd(l, lj) ≤ r and:

M ≡ (νd)(n[cL,r〈v〉.P ]l|∏

j∈Jnj [c(xj).Pj ]lj |M1)

andM ≡ (νd)(n[P ]l|

∏j∈J

nj [Pj{v/xj}]lj |M1).

By applying the definition of barb we conclude M ↓c@K .

25

3. The third part of the theorem is proved by induction on the derivationM

τ−→ JM ′Kθ.Suppose that M

τ−→ JM ′Kθ is due to an application of the rule (Move), thatmeans:

Active(P ) = false

n[P ]lτ−→ Jn[P ]lKµnl

,

hence , by applying (R-Move) we get:

Active(P ) = false

n[P ]l−→Jn[P ]lKµnl.

If Mτ−→ JM ′Kθ is due to an application of (Lose1):

McL![l,r]−−−−→ JM ′K∆M

τ−→JM ′K∆,

then, by applying Lemma 1, there exists n, v, P d such that c /∈ d and P , a(possibly empty) network M1 and two (possibly empty) sets J and K suchthat ∀i ∈ J ∪K d(l, li) ≤ r, such that:

M ≡ (νd)(n[out〈cL,r, v〉.P ]l|∏

j∈Jnj [in(c, xj).Pj ]lj |

∏k∈K

nk[c(xk).Pj ]lj |M1)

and

M ′ ≡ (νd)(n[cL,r〈v〉.P ]l|∏

j∈Jnj [c(xj).Pj ]lj |

∏k∈K

nk[Pk{⊥/xk}]lk |M1).

Finally, by applying rule (R-Bgn-Bcast), (R-Res) and (R-Struct) we get

M −→ JM ′Kθ.For the application of the rule (Lose2) the proof is analogous to the previousone.Suppose that M

τ−→ JM ′Kθ is due to the application of (Res):

M1τ−→ JM ′1Kθ

(νc)M1τ−→ J(νc)M ′1Kθ

.

By induction hypothesis M1 −→ JM ′1Kθ, hence, by applying rule (R-Res) we

get (νc)M1 −→ J(νc)M ′1Kθ.Finally, suppose that M

τ−→ JM ′Kθ is due to the application of (Par):

M1τ−→ JM ′1Kθ

M1|M2τ−→ JM ′1|M2Kθ

,

by induction hypothesis M1 −→ JM ′1Kθ, hence, by applying rule (R-Par) we

get M1|M2 −→ JM ′1|M2Kθ.

26

4. The last part of the theorem follows from definition of barb and Lemma

1. Formally, since Mc!v@K/R−−−−−−→ JM ′K∆ because M

cL!v[l,r]−−−−−→ JM ′K∆ for somelocation l, radius r and set L of intended recipients, by applying Lemma 1:

M ≡ (νd)(n[cL,r〈v〉.P ]l |∏

j∈Jnj [c(xj).Pj ]lj |M1)

andM ′ ≡ (νd)(n[P ]l |

∏j∈J

nj [Pj{v/xj}]lj |M1)

for some n, P , for some (possibly empty) sequence d such that c /∈ d, some(possibly empty) set J , and some (possibly empty) network M1. Then, byapplying the rule (R-End-Bcast), (R-Par) and (R-Res) we get

(νd)(n[cL,r〈v〉.P ]l |∏j∈Jnj [c(xj).Pj ]lj |M1) −→ J(νd)(n[P ]l |∏

j∈Jnj [Pj{v/xj}]lj |M1)K∆,

and, by applying (R-Struct), we obtain M −→ JM ′K∆, as required.

A.2 Soundness and Completeness of Bisimulation [Theorem ??]

Following we introduce two propositions that will be useful to prove sound-ness and completeness of bisimulation.

Proposition 2. Let M and N be two networks. If MRN for some bisimulationR w.r.t. FM, then for all scheduler F ∈ FM there exists a scheduler F ′ ∈ FMsuch that for all α and for all classes C in N/R it holds:

1. if α = τ or α = c!v@K / R then ProbFM (α

=⇒, C) = ProbF′

N (α

=⇒ C);2. if α = c?@l or α = c?ϑ@l then either ProbFM (

α=⇒, C) = ProbF

′

N (α

=⇒, C) or

ProbFM (α

=⇒, C) = ProbF′

N (=⇒, C).

Proof. We proceed by induction on the lenght of the weak transitionα

=⇒.If M reaches C in one step then, since MRN , ∃F ′ ∈ FM such that:

if α = τ or c!v@K / R, ProbFM (α−→, C) = ProbF

′

N (α

=⇒, C), while, if α = c?ϑ@l

or c?@l P robFM (α−→, C) = ProbF

′

N (α

=⇒, C), or ProbFM (α−→, C) = ProbF

′

N (=⇒, C), asrequired.

If M reaches C in more steps then we consider two cases:

– The first transition is α, and Mα−→ JM ′Kθ.

ProbFM (α

=⇒, C) =∑M∈spt(JM ′Kθ)(Prob

FM (

α−→, M)× ProbFM

(=⇒, C)).Now, if we partition the support of JM ′Kθ in equivalence classes of R, ∃Isuch that ∀i ∈ I Ci ∈ N/R, spt(JM ′Kθ) ∩ Ci 6= ∅, and spt(JM ′Kθ) ⊆

⋃i∈I Ci.

We get:

ProbFM (α

=⇒, C) =∑i∈I(Prob

FM (

α−→, Ci)× ProbFRepCi (=⇒, C)),

27

where RepCi is a representative element of the equivalence class Ci. Since

MRN , ∃F ∈ FM such that, ∀i ∈ I: if α = τ or c!v@K/R, ProbFM (α−→, Ci) =

ProbFN (α

=⇒, Ci), while, if α = c?ϑ@l or c?@l P robFM (α−→, Ci) = ProbFN (

α=⇒

, Ci), or ProbFM (α−→, Ci) = ProbFN (=⇒, Ci).

If we take F ′ ∈ LSched such that, ∀e such that e ≤prefix e′ ∈ ExecFN (α

=⇒, Ci), F ′(e) = F (e), and ∀e such that e ≤prefix e′ ∈ ExecFRepCi

(=⇒, C)F ′(e) = F (e) we get, if α = τ or c!v@K / R,

ProbFM (α

=⇒, C) =∑i∈I(Prob

FM (

α−→, Ci)× ProbFRepCi (=⇒, C))

=∑i∈I(Prob

F ′

N (α

=⇒, Ci)×ProbF′

RepCi(=⇒, C)) = ProbF

′

N (α

=⇒, C),while, if α = c?ϑ@l or c?@l:ProbFM (

α=⇒, C) =

∑i∈I(Prob

FM (

α−→, Ci)× ProbFRepCi (=⇒, C))=∑i∈I(Prob

F ′

N (α

=⇒, Ci)×ProbF′

RepCi(=⇒, C)) = ProbF

′

N (α

=⇒, C),or

=∑i∈I(Prob

F ′

N (=⇒, Ci)×ProbF′

RepCi(=⇒, C)) = ProbF

′

N (=⇒, C),and, by Definition 11, since both F , F ∈ FM, F ′ ∈ FM, as required.

– The first transition is a τ , and Mτ−→ JM ′Kθ.

The proof is analogous to the first item.

Proposition 3. Let R = (⋃i∈I Ri)∗, where Ri are Probabilistic Labelled Bisim-

ulations w.r.t. FM. Then R is a Probabilistic Labelled Bisimulation w.r.t. FM.

Proof. Each relation Ri partition the set N in equivalence classes. If (M,N) ∈Ri, that means (M,N) ∈ R, by definition of R. Given then an equivalenceclass Ci ∈ N/Ri, this is wholly contained in an equivalence class C ∈ N/R. Bypartitioning the equivalence class C with a set of equivalence classes for Ri, wecan then deduce the existence of a set J such that: C =

⋃j∈J Cij .

Now, let consider (M,N) ∈ R. That means (M,N) ∈ (⋃i∈I Ri)∗, and

(M,N) ∈ (⋃i∈I Ri)n for some n > 0.

We will prove by induction over n that R is a probabilistic labelled bisimu-lation.

– n = 1.If n = 1, (M,N) ∈ (

⋃i∈I Ri)1 means that for some i ∈ I, (M,N) ∈ Ri. We

have that ∃F ′ ∈ FM s.t. ∀α, C ∈ N/R :

If α = τ or c!v@K / R then ProbFM (α−→, C) =

∑j∈JProb

FM (

α−→, Cij)=∑j∈JProb

F ′

N (α

=⇒, Cij) = ProbF′

N (α

=⇒, C),as required.If α = c?ϑ or c?@l then:ProbFM (

α−→, C) =∑j∈JProb

FM (

α−→, Cij)=∑j∈JProb

F ′

N (α

=⇒, Cij) = ProbF′

N (α

=⇒, C),orProbFM (

α−→, C) =∑j∈JProb

FM (

α−→, Cij)=∑j∈JProb

F ′

N (=⇒, Cij) = ProbF′

N (=⇒, C),as required.

28

– n > 1.(M,N) ∈ (

⋃i∈I Ri)n means that ∃i ∈ I such that MRi(

⋃i∈I Ri)n−1N , and

that ∃O ∈ N such that, (M,O) ∈ Ri and (O,N) ∈ (⋃i∈I Ri)n−1.

(M,O) ∈ Ri implies that, ∀F ∈ FM ∃F1FM such that ∀C ∈ N/R and ∀α:

If α = τ or c!v@K / R then ProbFM (α−→, C) =

∑j∈JProb

FM (

α−→, Cij)

=∑j∈JProb

F1

O (α

=⇒, Cij) = ProbF1

O (α

=⇒, C),while, if α = c?ϑ@l or c?@l then:ProbFM (

α−→, C) =∑j∈JProb

FM (

α−→, Cij)=∑j∈JProb

F1

O (α

=⇒, Cij) = ProbF1

O (α

=⇒, C),orProbFM (

α−→, C) =∑j∈JProb

FM (

α−→, Cij)=∑j∈JProb

F1

O (=⇒, Cij) = ProbF1

O (=⇒, C).By induction hypothesis, ∀m < n, (

⋃i∈I Ri)m is a bisimulation, hence

(⋃i∈I Ri)n−1 is a bisimulation. Again, since for each (P,Q) ∈ (

⋃i∈I Ri)n−1,

(P,Q) ∈ R, and each equivalence class of (⋃i∈I Ri)n−1 is wholly contained

in an equivalence class for R, we can then partition C with a set of equiva-lence classes in (

⋃i∈I Ri)n−1 that means ∃J ′ such that C =

⋃j∈J′ Cj where

Cj ∈ N/(⋃i∈I Ri)n−1 ∀j ∈ J ′.

By proposition 2 we finally get that ∃F ′ ∈ FM such that ∀C ∈ N/R and∀α:If α = τ or c!v@K / R thenProbFM (

α−→, C) = ProbF1

O (α

=⇒, C) =∑j∈J′Prob

F1

O (α

=⇒, Cj)

=∑j∈J′ProbF

′

N (α

=⇒, Cj) = ProbF′

N (α

=⇒, C),while, if α = c?ϑ@l or c?@l then there are three different possibilities:ProbFM (

α−→, C) = ProbF1

O (α

=⇒, C) =∑j∈J′Prob

F1

O (α

=⇒, Cj)=∑j∈J′ProbF

′

N (α

=⇒, Cj) = ProbF′

N (α

=⇒, C),ProbFM (

α−→, C) = ProbF1

O (α

=⇒, C) =∑j∈J′Prob

F1

O (α

=⇒, Cj)=∑j∈JProb

F ′

N (=⇒, Cj) = ProbF′

O (=⇒, C),orProbFM (

α−→, C) = ProbF1

O (=⇒, C) =∑j∈J′Prob

F1

O (=⇒, Cj)=∑j∈JProb

F ′

N (=⇒, Cj) = ProbF′

O (=⇒, C).

Soundness. In order to prove that bisimulation is a sound characterisation of

Probabilistic Barbed Congruence we have to prove that ≈FMp is:

1. reduction closed w.r.t. FM2. probabilistic barb preserving w.r.t. FM3. contextual

Probabilistic Labelled Bisimulation is reduction closed.We have to prove that if M ≈FM

p N , then for all F ∈ FM, there exists

F ′ ∈ FM such that for all classes C ∈ N/R, ProbFM (C) = ProbF′

N (C).

29

By Theorem 1 and Definition 10 we deduce that ∃F ∈ FM such that

ProbFM (C) = ProbFM (=⇒, C′), where C′ = C ∪ {M ′ : M ′ ≡ M ′′ ∈ C}, but since∀M ′ such that M ′ ≡M ′′ ∈ C, by applying rule (R-Struct) M ′ ∼=FM

p M ′′, we get{M ′ : M ′ ≡M ′′ ∈ C} ⊆ C, that means C′ = C.

By Proposition 2 we have that ∃F ′ ∈ FM such that ProbFM (=⇒, C) =

ProbF′

N (=⇒, C).Finally, by Theorem 1 and Definition 10, ∃F ′ ∈ FM such that ProbF

′

N (=⇒, C) = ProbF

′

N (C), as required.

Probabilsitc Lablelled Bisimulation is Probabilistic barb preserving.To prove that bisimulation is Probabilistic barb preserving we have to show

that, if M ≈FMp N , then, for each scheduler F ∈ FM, for each channel c, and

for each set K of locations such that M⇓Fp c@K, then ∃F ′ ∈ FM such that

N⇓F′

p c@K.

Let M⇓Fp c@K for some channel c, some set K of locations, and scheduler

F ∈ FM. It means that ProbFM (H) = p, where M ′ ∈ H iff M ′ ↓c@K . We can

partition H in a set of equivalence classes for ≈FMp . Hence ∃I such that ∀i ∈ I

Ci ∈ N/ ≈FMp , Ci ∩H 6= ∅, and H ⊆

⋃i∈I Ci. We get:

ProbFM (H) =∑e∈ExecFM (H)P

FM (e) =

∑i∈I Prob

FM (Ci) = p.

by Theorem 1 and Definition 10, ∃F ∈ FM such that ∀i ∈ I:

ProbFM (Ci) = ProbFM (=⇒, C′i),where C′i = Ci ∪ {M ′ | ∃M ′′ ∈ Ci and M ′ ≡ M ′′}, but, since ∼=FM

p is closed

under structural congruence, ∀M ′ ≡M ′′ ∈ Ci, M ′ ∼=FMp M ′′, hence {M ′ : M ′ ≡

M ′′ ∈ Ci} ⊆ Ci, that means C′i = Ci. Hence:

ProbFM (Ci) = ProbFM (=⇒, Ci) ∀i ∈ I and∑i∈I Prob

FM (Ci) =

∑i∈I Prob

FM (=⇒, Ci).

Since M ≈FMp N by Definitions 10 and 11, ∃F ′ ∈ FM such that, ∀i ∈ I:

ProbFM (=⇒, Ci) = ProbF′

N (=⇒, Ci).Again by Lemma 1 and by Definition 10 ∃F ′ ∈ FM such that:

p =∑i∈I Prob

F ′N (=⇒, Ci) =

∑i∈I Prob

F ′

N (Ci) = ProbF′

N (H),

that means N⇓F′

p c@K as required.

Probabilistic Labelled Bisimulation is contextualWe start with the Parallel Composition. Let R be the following relation:

R = {(M | O,N | O) : M,N,M | O,N | O are well-formed, and ,M ≈FMp N}.

We will prove that it is a Probabilistic Labelled bisimulation w.r.t. FM. For thispurpose, we need to prove that, ∀F ∈ FM ∃F ′ ∈ FM such that, ∀C ∈ N/R, ∀α:

1. α = τ then ProbFM |O(τ−→, C) = ProbF

′

N |O(=⇒, C).If P,Q ∈ C, then, by definition of R, P ≡ P | O, Q ≡ Q | O and P ≈FM

p Q.

But then there exists D ∈ N/ ≈FMp such that D = {P : P | O ∈ C}. Now

we have three cases to consider:

30

(i) if M | O τ−→ JM | O′Kθ the proof is simple, because we have, ∀M inthe support of JM | O′Kθ, such that M ∈ C, M ≡ M | O′′ and, since

M ≈FMp N , N | O′′ ∈ C too, by definition of R. Hence (by applying rule

(Par) to the action Oτ−→ JO′Kθ), since N | O is well-formed, by Definition

11 ∃F ′ ∈ FM such that

ProbFM |O(τ−→, C) = ProbF

′

N |O(=⇒, C).

(ii) If M | O τ−→ JM ′ | OKθ, since M is well-formed, by Definition

11 ∃F1 ∈ FM such that ProbFM |O(τ−→, C) = ProbF1

M (τ−→,D). But since

M ≈FMp N , and N is well-formed, ∃F2 ∈ FM such that ProbF1

M (τ−→

,D) = ProbF2

N (=⇒,D). Again, since the network N | O is well-formed,

by Definition 11 ∃F ′ ∈ FM such that, by applying rule (Par) to theexecutions in ExecF2

N (=⇒,D), we get

ProbF2

N (=⇒,D) = ProbF′

N |O(=⇒, C).

(iii) If M | O τ−→ M ′ | O′ due to a synchronization between M and O,then there are two cases to consider.

If Mc!v[l,r]−−−−→ JM ′K∆ and O

c?v@k−−−−→ JO′K∆, for some message v, channel c,locations l, k and radius r, such that d(l, k) ≤ r, we can apply rule (Obs)

obtaining Mc!v@K/R−−−−−−→M ′ for some K ⊆ L and for some R, with k ∈ R.

Therefore, by Definition 11 ∃F1 ∈ FM such that:

ProbFM |O(τ−→, C) = ProbF1

M (c!v@K/R−−−−−−→,D).

But since N ≈FMp M , ∃F2 ∈ FM such that

ProbF1

M (c!v@K/R−−−−−−→,D) = ProbF2

N (c!v@K/R

=⇒ ,D),

where each execution e in ExecF2

N (c!v@K/R

=⇒ ,D) is of the form

e = Nτ−→θ1 N1 −→ ...Ni−1

c!v@K/R−−−−−−→∆ Ni −→ ...N ′,

and Ni−1c!v[l′,r′]−−−−−→∆ Ni for some l′ and r′ such that d(l′, k) ≤ r′. We

can apply rule (Bcast) obtaining Ni−1 | Oc!v[l′,r′]−−−−−→∆ Ni | O′ without

changing probability. Finally if we take F ′ ∈ LSched which applies rule(Lose2) to the output action, we obtain the required result:

ProbF2

N (c!v@K/R

=⇒ ,D) = ProbF′

N |O(=⇒, C),

and, by Definition 11 F ′ ∈ FM as required.

31

If Mc?v@k−−−−→ JM ′K∆ and O

c!v@K/R−−−−−−→ JO′K∆, for some message v, channelc, locations l, k and radius r, such that d(l, k) ≤ r, then by Definition 11M 6∈ M and ∃F1 ∈ FM such that:

ProbFM |O(τ−→, C) = ProbF1

M (c?v@k−−−−→,D).

Since N ≈FMp M , ∃F2 ∈ FM such that:

ProbF1

M (c?v@k−−−−→,D) = ProbF2

N (c?v@k=⇒ ,D)

orProbF1

M (c?v@k−−−−→,D) = ProbF2

N (=⇒,D).

In the first case, since by hypothesis k ∈ R and N | O is well-formed,also N is able to synchronize with O. Hence, again by Definition 11∃F ′ ∈ FM such that for all

e = Nτ−→θ1 N1 −→ ...Ni−1

c?v@k−−−−→ Ni −→ ...N ′ ∈ ExecF2

N (c?v@k=⇒ ,D)

there exists a matching execution such that, by applying rule (Bcast)

obtaining Ni−1 | Oc!v[l,r]−−−−→ Ni | O, and by applying rule (Lose2), is of

the form:

e′ = N | O τ−→θ1 N1 | O −→ ...Ni−1 | Oτ−→ Ni | O′ −→ ...N ′ | O′

in ExecF′

N |O(=⇒, C). Hence,

ProbF2

N (c?v@k=⇒ ,D) = ProbN |O(=⇒, C).

If N is not able to receive the message the proof is analogous: it is

sufficient to apply the rule (Par) to Oc!v@K/R−−−−−−→ JO′K∆, obtaining:

ProbF2

N (=⇒,D) = ProbN |O(=⇒, C).

2. α = c!v@K / RThe proof is analogous to the point (iii) of the previous item.

3. α = c?@k thenProbFM |O(

α−→, C) = ProbF′

N |O(α

=⇒, C) or ProbFM |O(α−→, C) = ProbF

′

N |O(=⇒, C).

If P,Q ∈ C, then P ≡ M | O, Q ≡ N | O and M ≈FMp N . But then

∃D ∈ N/ ≈FMp such that D = {M : M | O ∈ C}. Now we have two cases to

consider:(i) The transition is due to an action performed by O, hence O

α−→∆ O′

and M | O′ ∈ C. But since M ≈FMp N , N | O′ ∈ C too, ∃F ′ ∈ FM such

that by applying parallel composition to the input of O, we obtain thedesired result:

ProbFM |O(α−→, C) = ProbF

′

N |O(α

=⇒, C).

32

(ii) The transition is due to an action performed by M, in this case, byDefinition 11 ∃F1 ∈ FM such that:ProbFM |O(

α−→, C) = ProbF1

M (α−→,D). Since M ≈FM

p N ∃F2 ∈ FM suchthat:ProbF1

M (α−→,D) = ProbF2

N (α

=⇒,D),orProbF1

M (α−→,D) = ProbF2

N (=⇒,D).In both cases, since N | O is well-formed, by Definition 11 ∃F ′ such thatby applying parallel composition, we have:ProbF2

N (α

=⇒,D) = ProbF′

N |O(α

=⇒, C),orProbF2

N (=⇒,D) = ProbF′

N |O(=⇒, C)as required.

4. α = c?ϑ@k the proof is analogous as for α = c?@k.

Now we proceed with the Restriction. Let R = {((νd)M, (νd)N) : M ≈FMp

N} be a relation. We need to prove that it is a Probabilistic Labelled bisimulationw.r.t. FM.

Let consider C: if P,Q ∈ C, by definition of R, P ≡ (νd)P , Q ≡ (νd)Q and

P ≈FMp Q. But then ∃D ∈ N/ ≈FM

p such that D = {P : (νd)P ∈ C}.We have to prove that, ∀F ∈ FM ∃F ′ ∈ FM such that, ∀C ∈ N/R, ∀α:

1. α = τ implies that ProbF(νd)M (τ−→, C) = ProbF

′

(νd)N (=⇒, C).Since Chan(τ) = ⊥, by Definition 11 ∃F1 ∈ FM such that ProbF(νd)M (

τ−→, C) = ProbF1

M (τ−→,D) and, since M ≈FM

p N ∃F2 ∈ FM such that: ProbF1

M (τ−→

,D) = ProbF2

N (=⇒,D).

Finally we can take F ′ ∈ FM mimicking the executions in ExecF2

N (=⇒,D),when applying the restriction on N . Hence:

ProbF2

N (=⇒,D) = ProbF′

(νd)N (=⇒, C).

2. α = c!v@K / RSince d 6= c, by Definition 11 ∃F1 ∈ FM such that ProbF(νd)M (

α−→, C) =

ProbF1

M (α−→,D), then since M ≈FM

p N , ∃F2 ∈ FM such that

ProbF1

M (α−→,D) = ProbF2

N (α

=⇒,D).

Therefore, since Chan(α) 6= d, ∃F ′ ∈ FM such that:

ProbF2

N (α

=⇒,D) = ProbF′

(νd)N (α

=⇒, C).

3. α = c?@kAgain, since d 6= c, by Definition 11 ∃F1 ∈ FM such that ProbF(νd)M (

α−→, C) = ProbF1

M (α−→,D). Since M ≈FM

p N , there exists F2 ∈ FM such that

ProbF1

M (α−→,D) = ProbF2

N (α

=⇒,D) or

ProbF1

M (α−→,D) = ProbF2

N (=⇒,D).

33

In both cases we can apply rule (Res) to N, since Chan(τ) 6= Chan(α) 6= d.Therefore, by Definition 11 there exists F ′ ∈ FM such that the requiredresult holds, that isProbF2

N (α

=⇒,D) = ProbF′

(νd)N (α

=⇒, C) or

ProbF2

N (=⇒,D) = ProbF′

(νd)N (=⇒, C).4. α = c?ϑ@k

The proof is analogous as for α = c?@k.

Completeness. In order to prove the completeness of bismulation we show that

the relation R = {(M,N) : M ∼=FMp N} is a Probabilistic Labelled Bisimulation.

We have to prove that, ∀F ∈ FM ∃F ′ ∈ FM such that, ∀C ∈ N/R, ∀α:

if α = τ then ProbFM (τ−→, C) = ProbF

′

N (=⇒, C).By Theorem 1 and by Definition 10 we know that ProbFM (

τ−→, C) = ProbFM (C),and, since M ∼=FM

p N , ∃F ′ ∈ FM such that ProbFM (C) = ProbF′

N (C). Again

by Theorem 1 and Definition 10 ProbF′

N (C) = ProbF′

N (=⇒, C ∪ {N ≡ N ′ ∈C}), but since ∼=FM

p is closed under structural equivalence, ∀N ≡ N ′ ∈ C,N ∈ C, hence: ProbFM (

τ−→, C) = ProbF′

N (=⇒, C).if α = c!v@K / R then ProbFM (

α−→, C) = ProbF′

N (α

=⇒, C).First we notice that ProbFM (

c!v@K/R−−−−−−→, C) is either 0 or 1.

If ProbFM (c!v@K/R−−−−−−→, C) = 0 we are done, because it will be enough to take any

scheduler F ′ ∈ FM not allowing observable output actions on the channel

c, and we get ProbFM (c!v@K/R−−−−−−→, C) = ProbF

′

N (c!v@K/R

=⇒ , C).If ProbFM (

c!v@K/R−−−−−−→, C) = 1, then, by Definitions 11 and 6 ∃F ∈ FM such

that M⇓F1 c@K, and it means that ∃F ′ ∈ FM such that N⇓F′

1 c@K, hence

∃R′ such that K ⊆ R′ and Nc!v@K/R′

=⇒ . Now in order to mimic the effect ofthe action c!v@K / R, we build the following context

C[·] =∏n

i=1(ni[in(c, xi).[xi = v]out〈fiki,r, xi〉]ki | mi[in(fi, yi).out〈okiki,r, yi〉]ki),

where R = {k1, ..., kn} and C[0] 6∈ M.

Since Mc!v@K/R−−−−−−→, then the message is reachable by all nodes ni, hence, by

Definition 6 ∃F1 ∈ FM such that C[M ] −→∗M , where

M ≡M ′ |∏n

i=1(ni[0]ki | mi[out〈okiki,r, vi〉]ki),

with M 6↓f@R and M⇓F11 ok@R.

The absence of the barb on the channel f together with the presence ofthe barb on the channel ok ensures that all the locations in R have beenable to receive the message. Since C[M ] ∼=FM

p C[N ], ∃F2 ∈ FM such that

ProbF1

C[M ](C′) = ProbF2

C[N ](C′) where M ∈ C′.

34

Therefore, C[N ] −→∗N with N 6↓f@R and N⇓F2

1 ok@R. The constrains on thebarbs allow us to deduce that

N ≡ N ′ |∏n

i=1(ni[0]ki | mi[out〈okiki,r, vi〉]ki)

which implies Nc!v@K/R

=⇒ N ′, or N =⇒ N ′ in case (Lose2) has been appliedto the output action on the channel c. Since M, N ∈ C, then M ∼=FM

p N .

Since ∼=FMp is contextual, it results (νok)M ∼=FM

p (νok)N , from which we

can derive that M ′ ∼=FMp N ′. But since N ′ ∈ C and N

c!v@K/R=⇒ N ′, then, by

Definition 11 ∃F ′ ∈ FM such that:

ProbF′

N (c!v@K/R

=⇒ , C) = 1 = ProbFM (c!v@K/R

=⇒ , C).

if α = c?@k then there are two cases to consider. If M ∈ {M1, ...,Mn}, then

by Definition 10, there are no schedulers in FM allowing Mc?@k−−−→, hence,

by Definition 11, ProbFM (α−→, C) = 0 and it will be enough to take some

scheduler F ′ ∈ FM such that ProbF′

N (α

=⇒, C) = 0.

If M 6∈ {M1, ...,Mn}, we notice that ProbFM (c?v@k−−−−→, C) is either 0 or 1.

If ProbFM (c?@k−−−→, C) = 0 we are done, because it will be enough to take any

scheduler F ′ ∈ FM not allowing input actions on the channel c, and we get

ProbFM (c?@k−−−→, C) = ProbF

′

N (c?@k=⇒ , C).

If ProbFM (c?@k−−−→, C) = 1,we build the following context:

C[·] = · | m[out〈ck,r, v〉.out〈fk,r, v〉.out〈okk,r, v〉]k,

in order to mimic the behaviour of the networks, with m stationary, r > 0

and d(l, k) > r ∀l ∈ Loc s.t. l 6= k. But since Mc?@k−−−→ M ′, by Definitions

11 and 6 there exists a scheduler F1 ∈ FM such that:

C[M ] −→∗M ′ | m[out〈okk,r, v〉]k ∈ ExecF1

C[M ],

with M ′ | m[out〈okk,r, v〉]k 6↓f@k and M ′ | m[out〈okk,r, v〉]k⇓F11 ok@k. The

reduction sequence above must be matched by a corresponding reduction

sequence C[N ] −→∗N ′ | m[out〈okk,r, v〉]k, with

M ′ | m[out〈okk,r, v〉]k ∼=p N′ | m[out〈okk,r, v〉]k,

N ′ | m[out〈okk,r, v〉]k 6↓f@k and N ′ | m[out〈okk,r, v〉]k⇓F21 ok@k for some

F2 ∈ FM.This does not ensure that N actually performed the input action, but byDefinition 11 we can conclude that there exists F ′ ∈ FM and N ′ such

that either Nc?@k=⇒ N ′ or N =⇒ N ′. Since M ′ | m[out〈okk,r, v〉]k ∼=p N

′ |m[out〈okk,r, v〉]k and ∼=FM

p is preserved by restriction it follows that

(νok)(M ′ | m[out〈okk,r, v〉]k) ∼=FMp (νok)(N ′ | m[out〈okk,r, v〉]k),

35

from which we can easily derive M ′ ∼=FMp N ′ (applying rules for structural

equivalence), that means M ′, N ′ ∈ C and ∃F ′ ∈ FM such that:

ProbFM (c?@k−−−→, C) = 1 = ProbF

′

N (c?@k=⇒ , C)

orProbFM (

c?@k−−−→, C) = 1 = ProbF′

N (=⇒, C).

if α = c?ϑ@k the proof is analogous as for α = α = c?@k.

36