Probabilistic Mobility Models for Mobile and Wireless Networks^{⋆}

Lei Song and Jens Chr. Godskesen

IT University of Copenhagen Rued Langgaards Vej 7 DK-2300 Copenhagen S, Denmark

                            {leis,jcg}@itu.dk

Abstract. In this paper we present a probabilistic broadcast calculus for mobile and wireless networks whose connections are unreliable. In our calculus, broadcasted messages can be lost with a certain probability, and due to mobility the connection probabilities may change. If a network broadcasts a message from a location, it will evolve to a network distribution depending on whether nodes at other locations receive the message or not. Mobility of nodes is not arbitrary but guarded by a probabilistic mobility function (PMF), and we also define the notion of a weak bisimulation given a PMF. It is possible to have weak bisimular networks which have different probabilistic connectivity information. We furthermore examine the relation between our weak bisimulation and a minor variant of PCTL^{∗} [1]. Finally, we apply our calculus on a small example called the Zeroconf protocol [2].

1 Introduction

Mobile and wireless networks have gained in popularity in recent years, and the application area is broad, spanning from ambient intelligence, wireless local area networks, sensor networks, and cellular networks for mobile telephony. The key communication primitive in wireless communication is message broadcast but, differently from wired local area networks, broadcast in wireless networks is local, hence only nodes within the communication range of the emitting node can receive the message, and due to mobility the communication area may change over time.

Mobility and local wireless broadcast has been studied in the calculi: CBS♯[3], the ω-calculus[4], CMN[5], RBPT[6], and CMAN[7, 8]. All these calculi only deal with connectivity in two modes: either two nodes are connected or disconnected. It is often assumed that when a node at location l is within the transmission range of another node at location k, then the node at l can receive messages broadcasted from k with probability 1, otherwise with probability 0. Here we refine this assumption and equip a connection with a probability, since in an unreliable medium we cannot guarantee that the broadcasted messages will always be received even within the transmission range. For example, in Fig. 1 the dashed circle denotes the transmission range of k, every node at a location within the circle, such as l and m, may receive the messages broadcasted

⋆ Supported by the VKR Centre of Excellence MT-LAB

Fig. 1. Connectivity example.  Fig. 2. Equivalent connection probabilities.

from k, but the node at n outside the circle cannot. Intuitively, although both l and m are in the transmission range of k, it is more reasonable to let nodes there receive messages from k with different probabilities since m is further away from k than l. In our calculus, the connectivity of this network can be denoted as {{(0.9, l), (0.5, m), (0, n)} ⟼→ k} if nodes at l, m, n can receive messages from k with probability 0.9, 0.5, and 0 respectively.

In order to model mobility we let connection probabilities between locations change, and the changes are also probabilistic. For instance, the nodes at location m in Fig. 1 may move closer to location k with a certain probability in which case the nodes at m will be able to receive messages from k with a higher probability.

In practice, when verifying properties of a mobile network it will be reasonable to assume that mobility within a network is not arbitrarily but respects certain rules or distributions. Therefore we introduce a probabilistic mobility function (PMF) which defines the mobility rules of all the connections. A PMF returns the probability for a connection evolving from one value into another. For example, if in a PMF the connection probability from l to k is given by Fig. 2, then we know that it can change to 0.8 with probability 0.7 or stay at 0.9 with probability 0.3, that is:

\{\{(0.9, l), (0.5, m), (0, n)\} ⟼→ k\} −→ \begin{cases}0.7 : \{\{(0.8, l), (0.5, m), (0, n)\} ⟼→ k\} \\ 0.3 : \{\{(0.9, l), (0.5, m), (0, n)\} ⟼→ k\} \end{cases}

Hence we equip mobility with probabilities, and after each mobility action the network will evolve into a distribution with the probabilities specified by the given PMF. We expect that usually a PMF can be obtained based on measurement of case studies.

Our network calculus consists of concurrent processes (nodes) communicating internally over channels at (logical) locations and broadcasting messages to processes at neighboring locations over probabilistic connections that may change probabilistically over time as outlined above. The semantics is a combination of probability, concurrency, and non-determinism. Formally the labeled transition system semantics gives rise to a simple probabilistic automata as outlined in [9], which allows us to use a labeled variant of PCTL^{∗}[1] to reason about properties of networks specified in our calculus. We also define a (weak) bisimulation along the lines of [1] and show that it is sound and complete for our version of PCTL^{∗}. In our bisimulation, we abstract from mobility as in the other calculi for mobile and wireless systems mentioned above.

As a novelty a bisimulation is parameterized by a PMF, and since we abstract from mobility we consider two probabilities of a connection to be equivalent if they can evolve into each other eventually with probability 1 after a number of mobility steps. Intuitively, it means that a connection due to mobility can take any of the equivalent probabilities. For example, given the PMF in Fig. 2 the state 0.8 can evolve into 0.9 with probability 1 after an infinite number of steps. Furthermore, two locations l and m are considered equivalent if any other location k is connected to them by equivalent probabilities, because then nodes at k can with probability 1 receive messages from l and m with the same probability.

Another important contribution is the introduction of unknown probabilities. Since we are dealing with open systems where contexts may contain new nodes and information about connection probabilities, we cannot in a network expect to know the probability of all possible connections. We integrate unknown probabilities in our theory to deal with these cases. Intuitively a connection with an unknown probability means that the probability for the connection can be any value.

The paper is organized as follows: the syntax of our calculus is presented in the next section and in Section 3 we give the Labeled Transition System for it. In Section 4 a weak bisimulation is defined and we also prove it to be a congruence. PCTL^{∗} and its relation with weak bisimulation is given in Section 5. We illustrate the application of our calculus with a simple protocol called Zeroconf in Section 6. Finally, we end by a conclusion and future works.

2 The Calculus

Before introducing our calculus, we first give the following general definitions. A probability space is a triplet P = (Ω, F, η) where Ω is a set, F is a collection of subsets of Ω closed under complement and countable union that includes Ω. η : F → [0, 1] is a probability distribution such that η(Ω) = 1, and for any collection {C_{i}}_{i} of at most countably many pairwise disjoint elements of F, η(∪_{i}C_{i}) = ∑ _{i} η(C_{i}). A probability space (Ω, F, η) is discrete if Ω is countable and F = 2^{Ω}, and hence abbreviated as (Ω, η). Given probability spaces {P = (Ω_{i}, η_{i})}_{i∈I} and weights w_{i} > 0 for each i such that ∑ _{i∈I} w_{i} = 1, the convex combination ∑ _{i∈I} w_{i}P_{i} is defined as the probability space (Ω, η) such that Ω = ⋃ _{i∈I} Ω_{i} and for each set Y ⊆ Ω, η(Y) = ∑ _{i∈I} w_{i}η_{i}(Y ∩ Ω_{i}). We let {ρ_{i} : N_{i}}_{i∈I} denote the discrete probability space ({N_{i∈I}}, η) where η({N_{i}}) = ρ_{i}.

We presuppose a countably infinite set N of names, ranged over by x, y, z and a finite set L of location names, ranged over by k, l, m, n. The variables k̃, l̃…are used to denote a set of locations. In addition, we also suppose a finite set of probabilities ℘ including 0 and 1 ranged over by ρ, ρ′, ρ_{1} . . .. We define a location connection set, ranged over by , …, as a subset of {(ρ, l) | ρ ∈ ℘, l ∈ L}. We use l( ) = {l | (ρ, l) ∈ } to denote all the locations in . The syntax of processes is defined by the following grammar:

p, q ::= 0 | Act.p | if (x = y) then p else q | νxp | p||q | !p
Act ::= ⟨x⟩ | ȳ⟨x⟩ | (x) | y(x)

Action ⟨x⟩ represents broadcasting a message x, while the reception of a broadcasted message is denoted by (x); ȳ⟨x⟩ denotes sending a message x via the channel y and in

Table 1. Structural congruence.

⌊0⌋_{l} ≡ 0  ⌊!p⌋_{l} ≡ ⌊p||!p⌋_{l}  νxE||E′ ≡ νx(E||E′), if x fn(E′)
E||0 ≡ E  ⌊p||q⌋_{l} ≡ ⌊p⌋_{l}||⌊q⌋_{l}  ⌊if (x = x) then p else q⌋_{l} ≡ ⌊p⌋_{l}
⌊νx.p⌋_{l} ≡ νx⌊p⌋_{l}(E||E′)||E′′ ≡ E||(E′||E′′) ⌊if (x = y) then p else q⌋_{l} ≡ ⌊q⌋_{l}, x y
νxνyE = νyνxEE||F ≡ F||E { _{1} ⟼→ k}||{ _{2} ⟼→ k} ≡ { _{1} ∪ _{2} ⟼→ k}, l( _{1}) ∩ l( _{2}) = ∅

contrast y(x) represents receiving a message x on channel y. Process 0 is the deadlocked process; Act.p is the process that can perform action Act and then behave as p; if (x = y) then p else q behaves as p if names x and y match and as q otherwise; νxp means that name x is bounded in the process p; in composition p||q, the processes p and q can proceed in parallel and can also interact via shared names; !p means an unbounded number of parallel compositions of process p. As usual we often leave out a trailing 0.

The set of networks N is defined by the grammar:

E, F ::= 0 | ⌊p⌋_{l} | { ⟼→ l} | νxE | E||F

Here ⌊p⌋_{l} is a process p at location l; νxE and E||F are restriction and parallel composition respectively which have the standard meaning; { ⟼→ l} denotes connection information, i.e. if (ρ, k) ∈ , the node at location k is connected to l and can receive messages from l with probability ρ. We use E, F, G …to range over N.

We define a network distribution as a probability space = {(ρ_{i} : E_{i})}_{i∈I} meaning that a network can evolve into E_{i} with probability ρ_{i}. We use , , … to range over network distributions ND. If a network distribution consists of a single network, such as {(1 : E)}, then we denote it as E directly. Parallel composition of network distributions is defined by:

|| = {(ρ × ρ′: E||F) | (ρ : E) ∈ , (ρ′: F) ∈ }

A substitution {y/x} can be applied to a node, network or network distribution. When applied to a network distribution, it means applying this substitution to each network within this distribution. The set of free names and bound names in E, denoted by fn(E) and bn(E) respectively, are defined as expected. Structural congruence, ≡, is the least equivalence relation and congruence closed by the rules in Table 1 and α-conversion. ≡ is extended to network distributions as expected.

In the following, we use ρ_{k⟼→l} as an abbreviation of the probability from which k can receive messages from l. As mentioned, we assume that mobility is not arbitrary but respects certain rules. These rules are given by a function pf : L × L × ℘ × ℘ → ℘ called a probabilistic mobility function (PMF), the probability for ρ_{k⟼→l} changing from ρ to ρ′ is given by pf(k, l, ρ, ρ′). Let G_{k⟼→l}^{pf} be the underlying directed graph for ρ_{k⟼→l} given pf, where vertices are possible values of ρ_{k⟼→l} and where there is an edge from state ρ to ρ′ iff pf(k, l, ρ, ρ′) ∈ (0, 1], and we ignore nodes with 0 in-degree and 0 out-degree. Without causing any confusion, sometimes we also use G_{k⟼→l}^{pf} to denote the set of nodes in the graph called the support of ρ_{k⟼→l}. A PMF pf is valid if for all G_{k⟼→l}^{pf}, G_{k⟼→l}^{pf} ∅ and for each ρ ∈ G_{k⟼→l}^{pf}, ∑ _{ρ′∈G_{k⟼→l}^{pf}} pf(k, l, ρ, ρ′) = 1. In the following, we only consider valid PMFs.

A well-formed network under a given pf is defined inductively by: 0 and ⌊p⌋_{l} are well-formed, and νxE is well-formed if E is well-formed; { ⟼→ l} is well-formed if all location names in are distinct and for each (ρ, k) ∈ , ρ ∈ G_{k⟼→l}^{pf}; E||F is well-formed if both E, F are well-formed and for any l, k ∈ L with l k, there does not exist E′, F′ such that E ≡ {{(ρ, k)} ⟼→ l}||E′ and F ≡ {{(ρ′, k)} ⟼→ l}||F′. In the sequel given a pf we only consider the set of well-formed networks N_{pf}. We assume that every node can receive messages broadcasted by itself with probability 1, but for simplicity we often denote this implicitly.

We use ρ_{k⟼→l}(E) to denote the connection probability from k to l in network E, when the requested probability occurs in E it returns this value otherwise it returns θ_{k⟼→l} to denote an unknown probability, i.e.

ρ_{k⟼→l}(E) = \begin{cases}ρ & if there exists E′ s.t.E ≡ \{ ⟼→ l\}||E′ and (ρ, k) ∈ \\ θ_{k⟼→l} & otherwise \end{cases}

We use _{l}(E) to denote the set of all connection probabilities from some locations to l in E, that is _{l}(E) is the smallest set such that (ρ_{k⟼→l}(E), k) ∈ _{l}(E) if ρ_{k⟼→l}(E) ∈ ℘.

We generalize network distributions to contain unknown probabilities. Let θ̂_{k⟼→l} denote θ_{k⟼→l} or 1 − θ_{k⟼→l}. We let range over generalized probabilities, i.e. expressions being a finite sequence θ̂_{k_{0}⟼→l_{0}} × ... × θ̂_{k_{i}⟼→l_{i}} × ρ. We say that a generalized probability θ̂_{k_{0}⟼→l_{0}} × ... × θ̂_{k_{i}⟼→l_{i}} × ρ is 0 if ρ = 0. A generalized network distribution, GND, is defined inductively as follows: A network distribution is a GND, if = {( _{i} : E_{i})}_{i∈I} is a GND then (θ_{k⟼→l}× ) + ((1 − θ_{k⟼→l}) × ) = {(θ_{k⟼→l}× _{i} : E_{i}), (1 − θ_{k⟼→l}× _{i} : E_{i})}_{i∈I} is a GND. We may substitute unknown probabilities in a GND with known probabilities, e.g. ∘ _{l}(E) means replacing each unknown probability θ_{k⟼→l} in with the known probability ρ_{k⟼→l}(E) if (ρ_{k⟼→l}(E), k) ∈ _{l}(E).

3 Label Transition System

In this section we introduce the labeled transition system semantics for our calculus; the semantics is parameterized by a given PMF which is denoted by pf and left implicit throughout the rest of this section.

First we define a set of actions A, ranged over by α, by:

α ::= νx̃⟨x, ⟩@l | (x, ) ◁ l | νx̃ȳ⟨x⟩@l | y(x)@l | τ

νx̃⟨x, ⟩@l denotes that a node at location k receives the message x broadcasted from l with probability ρ if (ρ, k) ∈ ; (x, ) ◁ l means that the node at location k receives the message x from location l with probability ρ if (ρ, k) ∈ ; νx̃ȳ⟨x⟩@l means sending x on channel y at the location l (i.e.unicast), on the contrary y(x)@l means that x can be received on the channel y at location l. x̃ is either a singleton set {x} or empty, if x̃ is empty then x is free else it is bounded.

The labeled transition system is defined in Table 2; notice that the semantics is late, i.e. the bound names of an input become instantiated only when inferring a communication. Rules out, in, com, par, res, open, str are either standard or trivial and need no more comments; brd means that a process at a location can broadcast a message to the

Table 2. Labeled transition system.

(par) \frac{E ⟶^{α}}{E||F ⟶^{α} ||F} α ((x) ◁ l, νx̃⟨x⟩@l), bn(α) ∩ fn(F) = ∅

(out) \overline{⌊ȳ⟨x⟩.p⌋_{l} ⟶^{ȳ⟨x⟩@l} ⌊p⌋_{l}}  (open) \frac{E ⟶^{α} ′}{νxE ⟶^{νxα} ′} α ∈ \{ȳ⟨x⟩@l, ⟨x⟩@l\}, x y

(in) \overline{⌊y(x).p⌋_{l} ⟶^{y(x)@l} ⌊p⌋_{l}}  (com) \frac{E ⟶^{νz̃ȳ⟨z⟩@l} E′ F ⟶^{y(x)@l} F′}{E||F ⟶^{τ} νz̃(E′||F′\{z/x\})} z̃∩ fn(F) = ∅

(res) \frac{E ⟶^{α} ′}{νxE ⟶^{α} νx ′} x n(α)  (pro) \overline{\{ ⟼→ k\} ⟶^{(x, )◁k} \{ ⟼→ k\}}
(los) \overline{⌊Act.p⌋_{k} ⟶^{(x,∅)◁l} ⌊Act.p⌋_{k}} Act (y) and x fn(⌊Act.p⌋_{k})
(rec1) \overline{⌊(x).p⌋_{k} ⟶^{(x,∅)◁l} \{(θ_{k⟼→l} : ⌊p⌋_{k}), (1 − θ_{k⟼→l} : ⌊(x).p⌋_{k})\}}

(brd) \overline{⌊⟨x⟩.p⌋_{l} ⟶^{⟨x,∅⟩@l} ⌊p⌋_{l}} (rec2) \frac{E ⟶^{(x, )◁l}  F ⟶^{(x, )◁l}}{E||F ⟶^{(x, ∪ )◁l} ( ∘ _{l}(F))||( ∘ _{l}(E))}

(syn) \frac{E ⟶^{νỹ⟨y, ⟩@l}  F ⟶^{(x, )◁l}}{E||F ⟶^{νỹ⟨y, ∪ ⟩@l} (( ∘ _{l}(F))||( \{y/x\} ∘ _{l}(E)))} ỹ∩ (\{x\} ∪ fn(F)) = ∅

(con) \overline{\{\{(ρ, l)\} ⟼→ k\} ⟶^{τ} \{pf(l, k, ρ, ρ′) : \{\{(ρ′, l)\} ⟼→ k\}\}}(str) \frac{E ≡ F ⟶^{α} ≡}{E ⟶^{α}}

network it belongs to; rec1 states that nodes might evolve with unknown probability when they are ready to receive messages; rec2 allows to combine two networks which can receive a broadcasted message in parallel, and notice that unknown probabilities may be substituted by known ones. The union ∪ denotes that in a parallel composition the message can arrive at locations in both and with specific probabilities; syn deals with synchronization and broadcast, in that a network can broadcast a message to any neighbor network where each location may receive with a certain probability. For the same reason as in rec2, the location connection set in the resulting action is the union of the two location connection sets in the synchronizing actions. Notice that some processes must discard broadcasted messages as explained by the rules los.

In the rules rec2 and syn, we have that when parallelizing two networks, they can get connection information from each other and update the correspondent unknown probabilities. Note here that when there is a message broadcasted from l, we only need to update possibly unknown probabilities with probabilities from connections to l, that is why we only need D_{l}(E) and D_{l}(F) to update the unknown probabilities in rec2 and syn. The rule con changes the connection probabilities in a network depending on the

Fig. 3. A mobility transition.  Fig. 4. A bottom strongly connected component.

PMF parameterizing the semantics, and the rule pro contributes by revealing the current probabilistic connectivity information.

Example 1. Suppose we have a network E with ρ_{l⟼→k}(E) = 0.8 and we also know from the given PMF pf that pf(l, k, 0.8, 0.9) = 0.3, pf(l, k, 0.8, 0.7) = 0.2 and pf(l, k, 0.8, 0.8) = 0.5, then we have the derivation in Fig. 3 with ρ_{l⟼→k}(E_{1}) = 0.9, ρ_{l⟼→k}(E_{2}) = 0.7.

4 Weak Bisimulation

In this section we provide a weak bisimulation for our calculus.

A broadcast action, ⟨x, ⟩@l, contains the name of the broadcasting location, the broadcasted message, and a location connection set which denotes locations receiving the message with specific probabilities. We want to allow a network to simulate such an action by ⟨x, ⟩@m, if l and m are mobility equivalent. Intuitively, two locations are mobility equivalent if any of their connection probabilities, say ρ_{k⟼→l} and ρ_{k⟼→m}, are able to evolve into each other eventually with probability 1, in which case the node at location k can with probability 1 receive messages from l and m with the same probability. For example, if the mobility of ρ_{k⟼→l} = 0.8 and ρ_{k⟼→m} = 0.9 is given by Fig. 4, then ρ_{k⟼→l} can evolve into ρ_{k⟼→m} and vice versa. Otherwise, if the mobility of ρ_{k⟼→l} = 0.6 and ρ_{k⟼→m} = 0.5 is given by Fig. 5 then ρ_{k⟼→m} may evolve into ρ_{k⟼→l} but not the other way around.

The following definitions are used to define mobility equivalence between two locations in their respective networks.

A subgraph SGof G_{l⟼→k}^{pf} is called strongly connected if for each pair (ρ, ρ′) of states in SGthere exists a path fragment ρ_{0}ρ_{1} …ρ_{i} such that ρ_{j} ∈ SGand pf(l, k, ρ_{j}, ρ_{j+1} ) > 0 for 0 ≤ j < i with ρ = ρ_{0} and ρ′ = ρ_{i}. A strongly connected component (SCC) denotes a strongly connected set of states such that no proper superset of it is strongly connected. A bottom SCC (BSCC) is an SCC from which no state outside this SCC is reachable. If probabilities are in the same BSCC, they can for sure evolve into each other, or in probabilistic terms they can evolve into each other eventually with probability 1. For example, Fig. 4 is a BSCC whereas Fig. 5 and 6 are not. If two probabilities ρ and ρ′ are in the same BSCC within G_{l⟼→k}^{pf}, then we write pf(l, k, ρ, ρ′)^{∗} = 1.

Fig. 5. A non-SCC.  Fig. 6. A non-BSCC.

The eventual support of ρ_{l⟼→k} under a given PMF pf, denoted by ES^{pf}(l, k), is the set of all nodes (probabilities) which belong to a BSCC in G_{l⟼→k}^{pf}.

Definition 1. ES^{pf}(l, k) is consistent if G_{l⟼→k}^{pf} is a BSCC.

In the following, we use ⟦ ⟧_{ES^{pf}(l,k)} to denote the set of nodes of the BSCC of G_{l⟼→k}^{pf} which contains the node if ∈ ES^{pf}(l, k), here ⟦θ_{l⟼→k}⟧_{ES^{pf}(l,k)} = ES^{pf}(l, k) if ES^{pf}(l, k) is consistent, otherwise ⟦θ_{l⟼→k}⟧_{ES^{pf}(l,k)} = {θ_{l⟼→k}}.

Definition 2. Let pf be a PMF, then l in E and m in F are mobility equivalent, denoted by l_{E} ≍^{pf} m_{F}, if for any k ∈ L, either i) l = m with ρ_{k⟼→l}(E) = ρ_{k⟼→m}(F), or ii) ρ_{k⟼→l}(E) ∈ ES^{pf}(k, l) ∪ {θ_{k⟼→l}} and ρ_{k⟼→m}(F) ∈ ES^{pf}(k, m) ∪ {θ_{k⟼→m}} such that ⟦ρ_{k⟼→l}(E)⟧_{ES^{pf}(k,l)} = ⟦ρ_{k⟼→m}(F)⟧_{ES^{pf}(k,m)}.

That is, two locations l and m in E and F respectively are mobility equivalent if either a) the locations are identical and all other locations are connected to them in E and F with the the same (possibly unknown) connection probabilities, b) the probability for a connection to l belongs to a BSCC and the probability for the similar connection to m belongs to a BSCC with the same probabilities, if the probability for the connection to m is unknown in F, the eventual support for the connection must be consistent, or c) the probability for a connection to l is unknown in E, the eventual support ES for the connection is consistent, and the probability for the corresponding connection to m belongs to a BSCC with the same values as in ES. Intuitively, for the cases b) and c) it means that even though the connection probabilities for connections to l and m are not the same, then they eventually with probability 1 can evolve into each other by a number of mobility steps.

Example 2. Suppose the mobility rules for ρ_{l⟼→k} and ρ_{m⟼→k} are given by Fig. 6 and 4 respectively and let all other connection probabilities be permanently 1. Assume we are given two networks E and F such that ρ_{l⟼→k}(E) = 0.9, ρ_{m⟼→k}(F) = θ_{m⟼→k}. Then l_{E} ≍^{pf} m_{F}, but if ρ_{l⟼→k}(E) = 0.3 then l_{E} ^{pf} m_{F}, since there is no way for ρ_{m⟼→k}(F) to become 0.3.

It follows immediately from the definition of ≍^{pf} that it is an equivalence relation. Observe also that whenever ES^{pf}(l, k) is consistent, then the unknown connection probability θ_{l⟼→k} can be assigned with any value in ES^{pf}(l, k) while still preserving mobility equivalence.

In our weak bisimulation equivalence, we as usual abstract from internal steps which in our case also involve the probabilistic mobility steps changing connection probabilities. In order to capture that a connection probability for sure (with probability 1) can evolve into another, we introduce the relation →. Let → be the least relation closed by parallel composition, restriction and structural congruence and such that {{(ρ, l)} ⟼→ k} → {{(ρ′, l)} ⟼→ k} if pf(l, k, ρ, ρ′)^{∗} = 1.

We use E ⟹^{α} to denote that a distribution is reached through a finite sequence of steps some of which are internal. Formally ⟹^{α} is the least relation such that, E ⟹^{α}

iff (i) α = τ and E = , (ii) α = τ and E → , or (iii) there exists a step E ⟶^{β} ′ such that = ∑ _{(ρ:E′)∈ ′} ρ _{E′}, where E′ ⟹^{τ} _{E′} if β = α, otherwise E′ ⟹^{α} _{E′} and β = τ.

Since there might occur unknown probabilities during the evolution of networks, we have to resolve this in order to define our bisimulation. For that we introduce a set of networks denoted by Σ^{pf} and ranged over by σ^{pf}. The networks in Σ^{pf} only contain connection information for a given pf and it is defined by:

Σ^{pf} = { ||_{l∈L}{{(ρ, k) | k ∈ L} ⟼→ l} | ρ ∈ G_{k⟼→l}^{pf}}

We write E • σ^{pf} to denote a network behaving like E but obtaining new connection information from σ^{pf}, that is,

E • {∅ ⟼→ l} = E

E • \{\{(ρ, k)\} ∪ ⟼→ l\} = \{E • \{ ⟼→ l\} ρ_{k⟼→l}(E) θ_{k⟼→l} ; {(E||\{\{(ρ, k)\} ⟼→ l\}) • \{ ⟼→ l\} \atop otherwise}

The importance of mobility equivalence can be illustrated by the following lemma.

Lemma 1. For each σ^{pf} ∈ Σ^{pf}, if E • σ^{pf} ⟶^{(x, )◁l} and l_{E} ≍^{pf} m_{E} then E • σ^{pf} ⟹^{(x, )◁m} .

We lift the notion of equivalence relation to distributions in the usual way.

Definition 3. Let R be an equivalence relation over N_{pf}. Two (non-generalized) network distributions _{1} = (N_{pf}, η_{1}) and _{2} = (N_{pf}, η_{2}) are R-equivalent, written _{1} R _{2}, if η_{1}(C) = η_{2}(C) for each equivalence class C in N_{pf}/R.

Below follows our definition of weak bisimulation.

Definition 4. Given a PMF pf, an equivalence relation S ⊆ N_{pf} × N_{pf} is a weak bisimulation under pf if E S F implies l_{E} ≍^{pf} l_{F} for any l ∈ L and for each σ^{pf} ∈ Σ^{pf} whenever E • σ^{pf} ⟶^{α} then:

1. if α = y(x)@l then there exists F • σ^{pf} ⟹^{α} s.t. for each z ∈ N, {z/x} S {z/x}.

2. if α = (x, ) ◁ l then there exists F • σ^{pf} ⟹^{(x, )◁m} s.t. for each z ∈ N, {z/x} S {z/x} and l_{E} ≍^{pf} m_{F}.

3. if α = ⟨x, ⟩@l then there exists F • σ^{pf} ⟹^{⟨x, ⟩@m} s.t. S and l_{E} ≍^{pf} m_{F}.

4. otherwise there exists F • σ^{pf} ⟹^{α} and S .

Fig. 7. Network derivations.

Two networks E and F are weak bisimular under a given PMF pf, written E ≈_{pf} F, if E S F for some weak bisimulation S under pf.

Clauses 1 and 4 in Definition 4 are standard. Clause 2 requires that if nodes at locations l( ) in network E can receive a message from location l with specific probabilities, then nodes at locations l( ) in F must be able to receive the same message from some location m with the same probabilities which is mobility equivalent to l. Clause 3 means that if E can broadcast a message from l with receivers at locations l( ), then F can also broadcast the same message from some location m to l( ) with the same probabilities. In addition, l and m are required to be mobility equivalent. Notice that none of the resulting distributions in a bisimulation contains unknown probabilities because of σ^{pf}, and observe that all possible σ^{pf} are taken into account and hence all possible values of otherwise unknown connection information are considered.

Theorem 1. ≈_{pf} is a congruence.

To illustrate our weak bisimulation we give the following example.

Example 3. Suppose two nodes A = ⌊⟨x⟩⌋_{l}, B = ⌊(y).⟨y⟩⌋_{k} and connection information: P_{1} = {{0.8, k} ⟼→ l}, P_{2} = {{0.9, k} ⟼→ l}, P_{3} = {{1, k} ⟼→ l}. Let the mobility of ρ_{k⟼→l} be given by pf in Fig. 6. It is then not hard to see that A||B||P_{1} ≈_{pf} A||B||P_{2} ≈_{pf} A||B||P_{3}. The derivation is shown in Fig. 7 where we only show the essential transitions and omit others. Observe that in each of the three networks B can always receive the message from A with probability 0.8, 0.9, or 1.

5 Characterization

In this section we will examine the relation between our calculus and a variant of PCTL^{∗}

[1] which is a standard modal logic used for expressing properties of probabilistic systems. We use (E) to denote the probability of the equivalence class which contains E in a distribution and define the (weak) infinite paths of a network E under a given pf by:^{1}

Ω_{E} = {E_{0}α_{0}E_{1} …| ∃σ^{pf}.E_{0} = E • σ^{pf} ∧ ∀i ≥ 0 ∃ _{i+1}. E_{i} ⟹^{α_{i}} _{i+1} ∧ _{i+1}(E_{i+1}) 0}

For ω = E_{0}α_{0}E_{1}α_{1}... ∈ Ω_{E} we denote by ω|_{i} the finite path E_{0}α_{0}E_{1}...α_{i−1}E_{i} in which case we let ω|^{i} = E_{i}, and we define Ω_{E}|_{i} = {ω|_{i} | ω ∈ Ω_{E}}. Notice that as usual due to non-determinism we cannot define a probability measure on Ω_{E}. To resolve this we, like in e.g.[9, 10], define a policy. An i-level policy for Ω_{E} is a partial function

π_{i} : Ω_{E}|_{i} × A ↪ ND

defined by π_{i}(ω|_{i}, α) = if there exists ω|^{i} ⟹^{α} . A policy π for Ω_{E} is a pair consisting of a tuple of i-level policies one for each i ≥ 0 and σ^{pf} ∈ Σ^{pf} . It defines a subset of Ω_{E} denoted by Ω_{E}^{π} such that

Ω_{E}^{π} = {ω ∈ Ω_{E•σ^{pf}} | ∀i ≥ 0 ∃ , α, E. π_{i}(ω|_{i}, α) = ∧ (E) 0 ∧ ω|_{i+1} = ω|_{i}αE}

where π = ((π_{0}, π_{1}, …), σ^{pf}). The probability of a path E_{0}α_{0}E_{1}α_{1} … ∈ Ω_{E}^{π} is defined by ρ_{0}×ρ_{1}×…where for all i, π_{i}(E_{0}α_{0}E_{1}α_{1} …E_{i}, α_{i}) = for some and ρ_{i} = (E_{i+1}).

Let B_{E}^{π} be the smallest algebra of subsets of Ω_{E}^{π} that contains all the basic cylinder sets {ω ∈ Ω_{E}^{π} | ω|^{0} = E_{0} ∧ ... ∧ ω|^{i} = E_{i}} for all i ≥ 0 that is closed under complement and countable unions. ^{2} The measure on paths of Ω_{E}^{π}, written as μ_{π,E}, gives a unique measure on B_{E}^{π}.

Below we give the syntax and the semantics for our logic. Syntax. There are two kinds of formulas: state formulas Stat ranged over by ϕ, ϕ′ and sequence formulas Seqranged over by ψ, ψ′. The grammar is as follows:

ϕ ::= ⊤ | a | ¬ϕ | ϕ ∧ ϕ′ | ∃ψ | P_{▷◁q}ψ
ψ ::= α | ϕ | ¬ψ | ψ ∧ ψ′ | ◯ψ | ψUψ′

In the above, ▷◁ stands for one of =, ≤, ≥, <, >, q is a rational in [0,1] and α ∈ A. a ∈ AP where AP is the set of atomic propositions. Here we omit the details of AP and only assume that weak bisimular networks satisfy the same atomic propositions. These atomic propositions should also cover the connectivity of networks and be able to distinguish networks with non-equivalent connectivity. For example, if we have a network E such that ρ_{l⟼→k}(E) = 0.8 then we could say that E satisfy proposition ρ_{l⟼→k} = 0.8. Semantics. For a formula ϕ ∈ Stat, we indicate by E ⊧_{pf} ϕ its satisfaction on network E, and for ψ ∈ Seq its satisfaction on the path ω is denoted by ω ⊧_{pf} ψ under a given PMF pf. The semantics of the logical connectives are defined in the usual way; the

1 Notice that no path from a network E needs to be finite. 2 By standard measure theory this algebra is the Borel σ-algebra and all its elements are the measurable sets of paths.

Fig. 8. A home network.

semantics of the remaining operators is defined below:

ω ⊧_{pf} α iffω = E_{0}α_{0}E_{1} …∧ α_{0} =_{pf} α
ω ⊧_{pf} ◯ψ iffω = E_{0}α_{0}E_{1} …∧ E_{1}α_{1} …⊧_{pf} ψ
ω ⊧_{pf} ψUψ′ iffω = E_{0}α_{0}E_{1} …∧ ∃i ≥ 0.(E_{i}α_{i} …⊧_{pf} ψ′∧ ∀0 ≤ j < i.E_{j}α_{j} …⊧_{pf} ψ)
E ⊧_{pf} ∃ψ iff∃π, ω ∈ Ω_{E}^{π}. ω ⊧_{pf} ψ
E ⊧_{pf} P_{▷◁q}ψ iff∀π. μ_{π,E}({ω ∈ Ω_{E}^{π} | ω ⊧_{pf} ψ}) ▷◁ q

In the above ⟨x, ⟩@l =_{pf} ⟨x, ⟩@m iff l ≍^{pf} m, it is similar for receptions. Intuitively, E ⊧_{pf} P_{▷◁q}ψ denotes the probability for the path from E satisfying ψ is ▷◁ q. With this we can express many kinds of properties such as greatest and lowest bounds and intervals. For example, P_{≥q}ψ can be used to denote that the lowest bound is q while P_{≥q_{1}}ψ∧P_{<q_{2}}ψ guarantees that the probability is in interval [q_{1}, q_{2}) with q_{1} < q_{2}.

The following are the main results of this section which show the soundness and completeness of weak bisimulation with respect to PCTL^{∗}.

Theorem 2. If E ≈_{pf} F then for all ϕ ∈ Stat, E ⊧_{pf} ϕ iff F ⊧_{pf} ϕ.

Theorem 3. If for all ϕ ∈ Stat, E ⊧_{pf} ϕ iff F ⊧_{pf} ϕ, then E ≈_{pf} F.

6 The Zeroconf Protocol

The Zeroconf protocol is designed for self-configuring home local networks. For example, Fig. 8 gives a typical home local network which contains four nodes: PC1, PC2, Laptop, and PDA. The arrows indicate that PC1, PC2, and Laptop can receive messages from PDA with probability 0.9, 1, and 0.8 respectively. Here we assume that all other connections have probability 1.

In order to ensure mutual communication, each node must have an unique IP address, so when a new node joins a network it must be assigned an unused IP address. The Zeroconf protocol solves this in the following way:

1. The new node selects an IP address out of all available IP addresses randomly;

2. It broadcasts a message to other nodes to probe if the selected IP address is in use or not;

Table 3. The Zeroconf protocol.

oldnode_{ip} =!((x).(if x = ip then ⟨error⟩ else 0))

newnode_{i}^{p} = ⟨p⟩.waitawk_{i}^{p} newnode_{0}^{p} = ⟨success⟩ waitawk_{i}^{p} = (x).(if x = error then newnodeelse waitawk_{i}^{p}) + newnode_{i−1}^{p} newnode = νy(y(p).⟨p⟩.waitawk_{pn}^{p}|| ∏ _{ip∈IP} ȳ⟨ip⟩)

3. If the new node receives a message indicating the IP address is already taken, then it returns to step 1 and restarts the process;

4. Due to unreliable connections, messages can be lost with a certain probability. To increase the reliability of the protocol, the new node is required to send several probes for the same IP address;

5. If no error message has been received after these probes, the selected IP address will be used by the new node.

Note that after running the protocol it is indeed possible for a new node to use an IP address that is already used by another node. This is called address collision and is highly undesirable.

In the following, we model and analyse the Zeroconf protocol, the model of the protocol is given in Table 3.^{3} We use oldnode_{ip} to denote an existing network node, i.e. a process with IP address ip running at a location; oldnode_{ip} repeatedly receives messages and compare these messages with its own IP address ip. If a message is identical to ip, it will broadcast an error message, error, informing the new node that the selected IP address is being used already; newnode_{i}^{p} denotes a process which will probe i times before assuming that the selected IP address p is not used by other nodes. It will evolve into process waitawk_{i}^{p} after broadcasting a probe. newnode_{0}^{p} is a special process which denotes that the protocol succeeded in finding an unused IP address p (although this might not be true with a certain probability); waitawk_{i}^{p} waits for the responses from other nodes. If it receives an error message because the selected IP address is not valid, it will restart the whole process, otherwise it will recurse and become waitawk_{i}^{p} again. The summation here is used to denote timeout from waiting for responses and then start a new round of probing. newnodestarts the protocol by selecting an IP address from IP randomly, here IP is the set of all available addresses and ∏ means parallel composition of processes. In the above, we use pn to denote the maximum number of probes for the same IP address.

The behavior of the network in Fig. 8 can be represented as follows:

E = ⌊newnode⌋_{k} || ⌊oldnode_{ip_{1}}⌋_{l} || ⌊oldnode_{ip_{2}}⌋_{m} || ⌊oldnode_{ip_{3}}⌋_{n}

We assume Laptop, PC1, and PC2 are existing nodes which are located at l, m, and n respectively, and PDA at k is a node that wants to join the network; here ip_{1}, ip_{2}, and ip_{3} are used to denote IP addresses in IP already in use. Concerning mobility we assume a PMF pf such that the mobility rules of ρ_{k⟼→l} and ρ_{k⟼→m} are given by Fig. 4 and the

3 Summation is defined by: P + Q = νx(x̄⟨y⟩||x(y).P||x(y).Q).

mobility rule of ρ_{k⟼→n}is given by Fig. 6, in addition all the other connections are always equal to 1.

In the following, we use ⟨x⟩@l̃as a shorthand of ∨_{l∈l̃}⟨x, ⟩@l where ranges over all the location connection sets. With the PCTL^{∗} logic introduced in the above section, we can denote the obvious property that ”if an unused IP address is selected by the new node then the probability of this IP address being allocated to the new node is equal to 1”, formally we have:

ϕ = P_{=1}(∨_{ip∈IP\{ip_{1},ip_{2},ip_{3}}}⟨ip⟩@k → ♢(¬⟨error⟩@{l, m, n} ∧ ⟨success⟩@k))

letting ♢ψ =^{def} ⊤Uψ. Clearly E ⊧ ϕ. We may also specify the property: ”if an used IP address is selected by the new node then the probability of address collision is less than q”. Formally we have:

ϕ_{q} = P_{≤q}(∨_{i∈{1,2,3}}⟨ip_{i}⟩@kU ∨_{i∈{1,2,3}}⟨ip_{i}⟩@k → ♢(¬⟨error⟩@{l, m, n} ∧ ⟨success⟩@k))

Assuming the maximum number of probes pn to be 3 it turns out that E |̸= ϕ_{0.001} while E ⊧ ϕ_{0.008}. Intuitively, if the new node selects an used IP address such as ip_{1}, then among all policies to consider there exists a worst case policy under which oldnode_{ip_{1}} may fail to receive the probe from the new node for three times with probability (1 − 0.8)^{3} = 0.008.

In order to illustrate analysis through the use of weak bisimulation we may define

F ≡ ⌊newnode⌋_{k} || ⌊oldnode_{ip_{1}}⌋_{l} || ⌊oldnode_{ip_{3}}⌋_{m} || ⌊oldnode_{ip_{2}}⌋_{n}

i.e. compared to E in the network F the two old nodes PC1 and PC2 have swapped their locations m and n. Further let

E′ ≡ {{(k, 0.8)} ⟼→ l}||{{(k, 1)} ⟼→ m}||{{(k, 0.9)} ⟼→ n}

and let

F′ ≡ {{(k, 1)} ⟼→ l}||{{(k, 0.9)} ⟼→ m}||{{(k, 0.8)} ⟼→ n}

then because m_{E′} ≍^{pf} n_{F′} we infer

E||E′ ≈_{pf} F||F′

Intuitively, by the given pf locations m and n are mobility equivalent and furthermore they can always receive messages from other locations with the same probability. If the new node selecting an used IP address such as ip_{2} broadcasts a probe, then the node at location m in E can receive it with probability 1 and then broadcast an error message. The node at location n in F can simulate this by performing the same actions in addition with some mobility transitions. In both E and F, the newnodecan receive the error message with the same probability. A similar argument holds for other transitions.

7 Conclusion and Future Works

The main contribution of this paper is the development of a probabilistic broadcast calculus for mobile and wireless networks with unreliable connections in that broadcasted messages can be lost with a certain probability. Moreover, due to a probabilistic mobility function connections between locations may change with certain probabilities.

We have given a labeled transition system semantics for our calculus on which we define a probabilistic weak bisimulation equivalence parameterized by a probabilistic mobility function. Two bisimular networks need not have the same connectivity information and also they may broadcast the same messages from different locations. To the best of our knowledge, the integration of bisimulation, probabilistic loss of broadcasted messages, and probabilistic mobility functions is a novel contribution. Also, we have characterized our weak bisimulation by a variant of PCTL^{∗}.

A number of further developments are possible. One of them is that we could enrich the calculus by adding probability at the process level. This would allows to model e.g. randomized backoff protocols for wireless systems. Also the Zeroconf protocol example could be improved by having a randomized timeout instead of just using nondeterminism. Since time is important for wireless network, another extension is to consider a timed version of our calculus like in [11].

References

1. Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Weak Bisimulation is Sound and Complete for PCTL*. In: Brim, L., Jancar, P., Kretínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 355–370. Springer, Heidelberg (2002)

2. Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)

3. Nanz, S., Hankin, C.: A Framework for Security Analysis of Mobile Wireless Networks. Theoretical Computer Science. 367(1-2), 203–227 (2006)

4. Singh, A., Ramakrishnan, C.R, Smolka, S.A.: A Process Calculus for Mobile Ad Hoc Networks. In Olso, D. Lea, G. Zavattaro (eds.) COORDINATION 2008. LNCS, vol. 5052, pp. 296–314. Springer, Heidelberg (2008)

5. Merro, M.:An Observational Theory for Mobile Ad-hoc Networks. Electronic Notes in Theoretical Computer Scienc, vol. 173, pp. 275–293. Elsevier (2007)

6. Ghassemi, F., Fokkink, W., Movaghar, A.: Restricted Broadcast Process Theory. In: Proceedings of 6th Conference on Software Engineering and Formal Methods (SEFM’08), pp. 345– 354. IEEE Press (2008)

7. Godskesen, J.C.: A Calculus for Mobile Ad-hoc Networks. In Paphos, Murphy, A.L., Vitek, J. (eds.) COORDINATION’07. LNCS, vol. 4467, pp. 132–150. Springer, Heidelberg (2007)

8. Godskesen, J.C.: A Calculus for Mobile Ad-hoc Networks with Static Location Binding. In: 15th International Workshop on Expressiveness in Concurrency (2008)

9. Segala, R., Lynch, N.: Probabilistic Simulations for Probabilistic Processes. In Uppsala, Jonsson, B., Parrow, J. (eds.) CONCUR’94. LNCS, vol. 836, pp. 481–496. Springer, Heidelberg (1994)

10. Philippou, A., Lee, I., Sokolsky, O.: Weak Bisimulation for Probabilistic Systems. In PA, Palamidessi, C. (eds.) CONCUR’00. LNCS, vol. 1877, pp. 334–349. Springer, Heidelberg (2000)

11. Merro, M., Sibilio, E.: A Timed Calculus for Wireless Systems. In: 3rd International Conference on Fundamentals of Software Engineering (FSEN’09) (2009)