Connectivity and energy-aware preorders for mobile ad-hoc networks

Abstract

Network connectivity and energy conservation are two major goals in mobile ad-hoc networks (MANETs). In this paper we propose a probabilistic, energy-aware, broadcast calculus for the analysis of both such aspects of MANETs. We first present a probabilistic behavioural congruence together with a co-inductive proof technique based on the notion of bisimulation. Then we define an energy-aware preorder over networks. The behavioural congruence allows us to verify whether two networks exhibit the same (probabilistic) connectivity behaviour, while the preorder makes it possible to evaluate the energy consumption of different, but behaviourally equivalent, networks. In practice, the quantitative evaluation of the models is carried out by resorting to the statistical model checking implemented in the PRISM tool, i.e., a simulation of the probabilistic model. We consider two case studies: first we evaluate the performance of the Location Aided Routing protocol, then we compare the energy efficiency of the Go-Back-N protocol with that of the Stop-And-Wait in a network with mobility.

Appendix

Proof of Theorem 1

• 1. The first part is proved by induction on the reduction $M \xrightarrow {}\llbracket M'\rrbracket _{\theta }$.

  Let $M \xrightarrow {}\llbracket M'\rrbracket _{\theta }$ due to the application of the rule (R-Move). It means that $M \equiv M' \equiv n[P]_{l}$, for some name n, location l, some (possibly empty) process P, and $\theta = \mu _l^n$. We simply apply (Move) to obtain:

  $$\begin{aligned} \dfrac{}{n[P]_{l} \xrightarrow {\tau } \llbracket n[P]_{l}\rrbracket _{\mu _l^n}}. \end{aligned}$$

  Suppose that $M \xrightarrow {}\llbracket M'\rrbracket _{\theta }$ is due to the application of the rule (R-Par) with $M \equiv M_1\mid M_2$, $M' \equiv M_1'\mid M_2$ and:

  $$\begin{aligned} \dfrac{M_1 \xrightarrow {}\llbracket M_1'\rrbracket _{\theta }}{M_1\mid M_2 \xrightarrow {}\llbracket M_1'\mid M_2\rrbracket _{\theta }}. \end{aligned}$$

  By induction hypothesis there exist $N \equiv M_1$ and $N' \equiv M_1'$ such that $N \xrightarrow {\tau } \llbracket N'\rrbracket _{\theta }$, then by applying rule (Par) we get:

  $$\begin{aligned} \dfrac{N \xrightarrow {\tau } \llbracket N'\rrbracket _{\theta }}{N \mid M_2 \xrightarrow {\tau } \llbracket N'\mid M_2\rrbracket _{\theta }}, \end{aligned}$$

  hence by the rules of structural congruence we have that $N \mid M_2 \equiv M_1 \mid M_2 \equiv M$ and $N' \mid M_2 \equiv M_1' \mid M_2 \equiv M'$.

  Suppose that $M \xrightarrow {}\llbracket M'\rrbracket _{\theta }$ is due to the application of the rule (R-Res) with $M \equiv (\nu c)M_1$ and $M' \equiv (\nu c) M_1'$ for some channel c and some networks $M_{1}$ and $M_{1}'$, then

  $$\begin{aligned} \dfrac{M_1 \xrightarrow {}\llbracket M_1'\rrbracket _{\theta }}{(\nu c) M_1 \xrightarrow {}\llbracket (\nu c) M_1'\rrbracket _{\theta }}. \end{aligned}$$

  By induction hypothesis there exist $N \equiv M_1$ and $N' \equiv M_1'$ such that $N \xrightarrow {\tau } \llbracket N'\rrbracket _{\theta }$, then by applying rule (Res), since ${\mathtt {Chan}}(\tau ) \ne c$ we get:

  $$\begin{aligned} \dfrac{N \xrightarrow {\tau } \llbracket N'\rrbracket _{\theta }}{(\nu c) N \xrightarrow {\tau } \llbracket (\nu c) N'\rrbracket _{\theta }}, \end{aligned}$$

  hence by the rules of structural congruence we have that $(\nu c) N \equiv (\nu c) M_{1} \equiv M$ and $(\nu c) N' \equiv (\nu c) M_{1}' \equiv M'$.

  Let $M \xrightarrow {}\llbracket M'\rrbracket _{\theta }$ due to the application of the rule (R-Bcast). Then $M \equiv n[\bar{c}_{L, r} \langle \tilde{v} \rangle .P]_{l} \mid \prod _{i \in I} n_i[c(\tilde{x}_i).P_i]_{l_i}$ and $M' \equiv n[P]_{l} \mid \prod _{i \in I} n_i[P_i\{\tilde{v}/\tilde{x}_i\}]_{l_i}$ for some name n, channel c, location l, radius r, some set L of locations, some tuple $\tilde{v}$ of messages, some (possibly empty) process P, some (possibly empty) set I of networks. By applying the rules (Snd), (Rcv), $\mid I\mid$ times the rule (Bcast) and, finally the rule (Lose), we obtain

  $$\begin{aligned}&n[\bar{c}_{L, r} \langle \tilde{v} \rangle .P]_{l} \mid \prod _{i \in I} n_i[c(\tilde{x}_i).P_i]_{l_i}{\xrightarrow {\tau }} \\&\quad \llbracket n[P]_{l} \mid \prod _{i \in I} n_i[P_i\{\tilde{v}/\tilde{x}_i\}]_{l_i} \rrbracket _{\varDelta }\,. \end{aligned}$$

  Finally, suppose that the reduction $M \xrightarrow {}\llbracket M'\rrbracket _{\theta }$ is due to an application of rule (R-Struct):

  $$\begin{aligned} \dfrac{ M \equiv N \quad N {\xrightarrow {}} \llbracket N' \rrbracket _{\theta } \quad N' \equiv M' }{M {\xrightarrow {}} \llbracket M' \rrbracket _{\theta }}. \end{aligned}$$

  By induction hypothesis there exist $N_{1} \equiv N$ and $N_{2} \equiv N'$ such that $N_{1} \xrightarrow {\tau } \llbracket N_{2}\rrbracket _{\theta }$. The statement follows since by applying the rules of the structural congruence we have $M \equiv N \equiv N_{1}$ and $M' \equiv N' \equiv N_{2}$.

• 2. The second part of the theorem follows straightforwardly from Lemma 1 and the definition of Barb.

  • $\Rightarrow$ If $M \downarrow _{c@K}$, by the definition of Barb:

    $$\begin{aligned} M \equiv (\nu \tilde{d}) (n[\bar{c}_{L,r} \langle \tilde{v} \rangle .P]_{l} \mid M_1)\,, \end{aligned}$$

    for some n, $\tilde{v}$, L, r, some (possibly empty) sequence $\tilde{d}$ with $c \notin \tilde{d}$, some process P and some (possibly empty) network $M_1$, with $K \subseteq \{ k \in L \text{ such } \text{ that } d(l,k) \le r\}$ and $K \ne \emptyset$. By applying the rules (Snd), (Par) and (Res):

    $$\begin{aligned} \dfrac{n[\bar{c}_{L,r} \langle \tilde{v} \rangle .P]_{l} \xrightarrow {c_{L}!\tilde{v}[l,r]} \llbracket n[P]_{l}\rrbracket _{\varDelta }}{M \xrightarrow {c_{L}!\tilde{v}[l,r]} \llbracket (\nu \tilde{d}) (n[P]_{l} \mid M_1\rrbracket _{\varDelta })}; \end{aligned}$$

    then by rule (Obs): $n[\bar{c}_{L,r} \langle \tilde{v} \rangle .P]_{l}\mid M_1 \xrightarrow {c!\tilde{v}@K \triangleleft R} \llbracket n[P]_{l}\mid M_1\rrbracket _{\varDelta },$ where $R = \{l' \in { Loc }: d(l,l') \le r\}$, and $K \subseteq L \cap R$ as required.

  • $\Leftarrow$ If $M \xrightarrow {c!\tilde{v}@K \triangleleft R} \llbracket M'\rrbracket _{\varDelta }$, because $M \xrightarrow {c_L!\tilde{v}![l,r]} \llbracket M'\rrbracket _{\varDelta }$, by applying Lemma 1 there exist n, some (possibly empty) sequence $\tilde{d}$ such that $c \notin \tilde{d}$, some process P, some (possibly empty) network $M_{1}$ and a set I, such that $\forall i \in I$ with $d(l,l_i) \le r$:

    $M \equiv (\nu \tilde{d}) (n[\bar{c}_{L,r} \langle \tilde{v} \rangle .P]_{l} | \prod _{i \in I} n_i[c(\tilde{x}_i).P_i]_{l_i} \mid M_1)$ and $M' \equiv (\nu \tilde{d}) (n[P]_{l} |\prod _{i \in I} n_i[P_i\{\tilde{v}/\tilde{x}_i\}]_{l_i} \mid M_1).$

    Since $K \ne \emptyset$, by the definition of barb we conclude $M \downarrow _{c@K}$.

• 3. The third part of the theorem is proved by induction on the derivation $M \xrightarrow {\tau } \llbracket M' \rrbracket _{\theta }$.

  Suppose that $M \xrightarrow {\tau } \llbracket M' \rrbracket _{\theta }$ is due to an application of the rule (Move), i.e., $M \equiv n[P]_{l}$, $M' \equiv n[P]_{l}$, for some name n, some (possibly empty) process P, some location l, $\theta = {\mu }^n_l$ and

  $$\begin{aligned} \dfrac{ }{n[P]_{l} \xrightarrow {\tau } \llbracket n[P]_{l} \rrbracket _{{\mu }^n_l}}, \end{aligned}$$

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

  $$\begin{aligned} \dfrac{}{n[P]_{l} {\xrightarrow {}} \llbracket n[P]_{l}\rrbracket _{\mu ^{n}_{l}}}. \end{aligned}$$

  If $M \xrightarrow {\tau } \llbracket M' \rrbracket _{\theta }$ is due to an application of (Lose):

  $$\begin{aligned} \dfrac{M \xrightarrow {c_L!\tilde{v}[l,r]} \llbracket M' \rrbracket _{\varDelta }}{M {\xrightarrow {\tau }} \llbracket M' \rrbracket _{\varDelta }}, \end{aligned}$$

  for some channel c, some set L of locations, some tuple $\tilde{v}$ of messages, some location l and radius r. By applying Lemma 1, there exist n, $\tilde{v}$, a (possibly empty) sequence $\tilde{d}$ such that $c \notin \tilde{d}$, a process P, a (possibly empty) network $M_1$ and a (possibly empty) set I with $d(l,l_i) \le r \forall i \in I$ such that:

  $$\begin{aligned} M\equiv (\nu \tilde{d}) (n[\bar{c}_{L,r} \langle \tilde{v} \rangle .P]_{l} | \prod _{i \in I} n_i[c(\tilde{x}_i).P_i]_{l_i} \mid M_1) \end{aligned}$$

  and

  $$\begin{aligned} M' \equiv (\nu \tilde{d}) (n[\bar{c}_{L,r} \langle \tilde{v} \rangle .P]_{l} | \prod _{i \in i} n_i[P_i\{\tilde{v}/\tilde{x}_i\}]_{l_i} \mid M_1)\,. \end{aligned}$$

  Finally, by applying rules (R-Bcast), (R-Res) and (R-Struct) we get $M \xrightarrow {}\llbracket M' \rrbracket _{\theta }$. Suppose that $M \xrightarrow {\tau } \llbracket M' \rrbracket _{\theta }$ is due to the application of (Res) with $M \equiv (\nu c) M_1$ and $M' \equiv (\nu c) \llbracket M_1'\rrbracket _{\theta }$, for some channel c and for some networks $M_{1}$ and $M_{1}'$. Then we have:

  $$\begin{aligned} \dfrac{M_1 \xrightarrow {\tau } \llbracket M_1' \rrbracket _{\theta } }{(\nu c) M_1 \xrightarrow {\tau } \llbracket (\nu c) M_1'\rrbracket _{\theta }}. \end{aligned}$$

  By induction hypothesis $M_1 \xrightarrow {}\llbracket M_1' \rrbracket _{\theta }$, hence, by applying rule (R-Res) we get $(\nu c) M_1 \xrightarrow {}\llbracket (\nu c) M_1'\rrbracket _{\theta }$. Finally, suppose that $M \xrightarrow {\tau } \llbracket M' \rrbracket _{\theta }$ is due to the application of (Par) with $M \equiv M_{1} \mid M_{2}$, $M' \equiv M_{1}' \mid M_{2}$ and

  $$\begin{aligned} \dfrac{M_1 \xrightarrow {\tau } \llbracket M_1' \rrbracket _{\theta } }{M_1|M_2 \xrightarrow {\tau } \llbracket M_1'|M_2\rrbracket _{\theta }}. \end{aligned}$$

  By induction hypothesis $M_1 \xrightarrow {}\llbracket M_1' \rrbracket _{\theta }$, hence, by applying rule (R-Par) we get $M_1|M_2 \xrightarrow {}\llbracket M_1'|M_2\rrbracket _{\theta }$.

• 4. The last part of the theorem follows from the definition of barb and Lemma 1. Indeed, since $M \xrightarrow {c!\tilde{v}@K \triangleleft R}\llbracket M'\rrbracket _{\varDelta }$ because $M \xrightarrow {c_L!\tilde{v}[l,r]} \llbracket M'\rrbracket _{\varDelta }$ for some location l, radius r and set L of intended recipients, by applying Lemma 1, there exist n, a (possibly empty) sequence $\tilde{d}$ with $c \notin \tilde{d}$, a process P, a (possibly empty) network $M_{1}$ and a (possibly empty) set I such that:

  $$\begin{aligned} M \equiv (\nu \tilde{d}) (n[\bar{c}_{L,r} \langle \tilde{v} \rangle .P]_{l} \mid \prod _{i \in I} n_i[c(\tilde{x}_i).P_i]_{l_i} \mid M_1) \end{aligned}$$

  and

  $$\begin{aligned} M' \equiv (\nu \tilde{d}) (n[P]_{l} \mid \prod _{i \in I} n_i[P_i\{\tilde{v}/\tilde{x}_i\}]_{l_i} \mid M_1)\,. \end{aligned}$$

  Then, by applying the rules (R-Bcast), (R-Par) and (R-Res) we get:

  $(\nu \tilde{d}) (n[\bar{c}_{L,r} \langle \tilde{v} \rangle .P]_{l} \mid \prod _{i \in I} n_i[c(\tilde{x}_i).P_i]_{l_i} \mid M_1)\xrightarrow {}\llbracket (\nu \tilde{d}) (n[P]_{l} \mid \prod _{i \in I} n_i[P_i\{\tilde{v}/\tilde{x}_i\}]_{l_i} \mid M_1)\rrbracket _{\varDelta },$

  and, by applying (R-Struct), we obtain $M \xrightarrow {}\llbracket M'\rrbracket _{\varDelta }$, as required. $\square$

Proof of Theorem 2

We have to prove that $\approx _p^{{\mathcal {F}}}$ is:

• 1. probabilistic barb preserving

• 2. reduction closed

• 3. contextual.

$\mathrm {1.}$ To prove that the probabilistic labelled bisimilarity $\approx _p^{{\mathcal {F}}}$ is barb preserving we have to show that if $M \approx _p^{{\mathcal {F}}} N$ then, for each scheduler $F \in {{\mathcal {F}}}_{{\mathcal {C}}}$, for each channel c and for each set K of locations such that $M {\Downarrow }_{p}^{F}{c@K}$, there exists $F' \in {{\mathcal {F}}}_{{\mathcal {C}}}$ such that $N {\Downarrow }_{p}^{F'}{c@K}$.

Assume that $M {\Downarrow }_{p}^{F}{c@K}$ for some $F \in {\mathcal {F}}_{{\mathcal {C}}}$. By Definition 3 we have $Prob_M^F(H)=p$, where $H = \{M':M' \downarrow _{c@K}\}$. We can partition H into a set of equivalence classes with respect to $\approx _p^{{\mathcal {F}}}$. Formally, $\exists J$ such that $H\subseteq \cup _{j \in J} {\mathcal {C}}_j$, and $\forall j \in J$ we have ${\mathcal {C}}_{j} \in {\mathcal {N}}/\cong _{p}^{{\mathcal {F}}}$ and $H \cap {\mathcal {C}}_{j} \ne \emptyset$. Hence:

$$\begin{aligned} Prob_M^F(H)= {\sum }_{e \in Exec_M^F(H)} P_M^F(e) = {\sum }_{j \in J} Prob_M^F({\mathcal {C}}_j) = p. \end{aligned}$$

By Theorem 1 and by Definition 8 there exists $\hat{F} \in \hat{{\mathcal {F}}}_{{\mathcal {C}}}$ such that $\forall j \in J$:

$$\begin{aligned} Prob_M^F({\mathcal {C}}_j) = Prob_M^{\hat{F}}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}}, {\mathcal {C}}_j') \end{aligned}$$

where ${\mathcal {C}}_j' = {\mathcal {C}}_j \cup \{\hat{M} \mid \exists \hat{M'} \in {\mathcal {C}}_j \text{ and } \hat{M} \equiv \hat{M'} \}$.

Now, since $\forall \hat{M}$ such that $\hat{M} \equiv \hat{M'} \in {\mathcal {C}}_j$, by applying rule (R-Struct) and by Definition 4 $\hat{M} \cong _p^{{\mathcal {F}}} \hat{M'}$, we obtain that $\{\hat{M}:\hat{M} \equiv \hat{M'} \in {\mathcal {C}}_j\} \subseteq {\mathcal {C}}_j$, that means ${\mathcal {C}}_j' = {\mathcal {C}}_j \forall j \in J$. Hence we get:

$$\begin{aligned} {\sum }_{j \in J} Prob_M^F({\mathcal {C}}_j) = {\sum }_{j \in J} Prob_M^{\hat{F}}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}}, {\mathcal {C}}_j). \end{aligned}$$

Since $M \approx _p^{{\mathcal {F}}} N$, there exists $\hat{F'} \in \hat{{\mathcal {F}}}_{{\mathcal {C}}}$ such that, by Proposition 2, for all $j \in J$: $Prob_M^{\hat{F}}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}}, {\mathcal {C}}_j) = Prob_N^{\hat{F'}}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}}, {\mathcal {C}}_j)$. We then have:

$$\begin{aligned} p = {\sum }_ {j \in J} Prob_N^{\hat{F'}}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}}, {\mathcal {C}}_j). \end{aligned}$$

Again, by Theorem 1, Proposition 2 and Definition 4, there exists $F' \in {\mathcal {F}}_{{\mathcal {C}}}$ such that for all $j \in J$: $Prob_N^{\hat{F'}}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}}, {\mathcal {C}}_j) = Prob_N^{F'}({\mathcal {C}}_j)$ and

$$\begin{aligned} p = {\sum }_ {j \in J} Prob_N^{\hat{F'}}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}},{\mathcal {C}}_j) = {\sum }_ {i \in J} Prob_N^{F'}({\mathcal {C}}_j) = Prob_N^{F'}(H)\, \end{aligned}$$

i.e., $N {\Downarrow }_{p}^{F'}{c@K}$ as required.

$\mathrm {2.}$ To prove that probabilistic labelled bisimilarity $\approx _p^{{\mathcal {F}}}$ is reduction closed, we have to show that if $M \approx _p^{{\mathcal {F}}} N$, then for all $F \in {\mathcal {F}}_{{\mathcal {C}}}$, there exists $F' \in {\mathcal {F}}_{{\mathcal {C}}}$ such that for all classes ${\mathcal {C}}\in {\mathcal {N}}/\cong _{p}^{{\mathcal {F}}}$, $Prob_M^F({\mathcal {C}}) = Prob_N^{F'}({\mathcal {C}}).$

By Theorem 1 and by Definition 8 we have that $\exists \hat{F} \in \hat{{\mathcal {F}}}_{{\mathcal {C}}}$ such that $Prob_M^F({\mathcal {C}}) = Prob_M^{\hat{F}}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}}, {\mathcal {C}}')$, where ${\mathcal {C}}' = {\mathcal {C}} \cup \{\hat{M}: \hat{M} \equiv \hat{M'} \in {\mathcal {C}}\}$, but since $\forall \hat{M}$ such that $\hat{M} \equiv \hat{M'} \in {\mathcal {C}}$, by applying rule (R-Struct) and by Definition 4 $\hat{M} \cong _p^{{\mathcal {F}}} \hat{M'}$ we get $\{\hat{M}:\hat{M} \equiv \hat{M'} \in {\mathcal {C}}\} \subseteq {\mathcal {C}}$, i.e., ${\mathcal {C}}' = {\mathcal {C}}$.

By Proposition 2 we have that there exists $\hat{F}' \in \hat{{\mathcal {F}}}_{{\mathcal {C}}}$ such that $Prob_M^{\hat{F}}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}}, {\mathcal {C}}) = Prob_N^{\hat{F'}}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}}, {\mathcal {C}})$.

Finally, by Theorem 1 and by Definitions 8 and 4, $\exists F' \in {\mathcal {F}}_{{\mathcal {C}}}$ such that $Prob_N^{\hat{F}'}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}}, {\mathcal {C}}) = Prob_N^{F'}({\mathcal {C}})$, as required.

$\mathrm {3.}$ In order to prove that probabilistic labelled bisimilarity $\approx _p^{{\mathcal {F}}}$ is contextual we have to prove that, if $M \approx _p^{{\mathcal {F}}} N$:

• 1. $M \mid O \approx _p^{{\mathcal {F}}} N \mid O \forall O \in {\mathcal {N}}$.

• 2. $(\nu d) M \approx _p^{{\mathcal {F}}} (\nu d) N \forall d \in {\mathbf {C}}$.

Case 1. Let us consider the relation

$$\begin{aligned} {\mathcal {R}} = \{(M\mid O, N \mid O) : M \approx _{p}^{{\mathcal {F}}} N \}. \end{aligned}$$

We prove that for all scheduler $F \in \hat{{\mathcal {F}}}_{{\mathcal {C}}}$ there exists a scheduler $F' \in \hat{{\mathcal {F}}}_{{\mathcal {C}}}$ such that for all $\alpha$ and for all classes ${\mathcal {C}}$ in ${\mathcal {N}}/{\mathcal {\approx }}_p^{{\mathcal {F}}}$:

• 1. if $\alpha = \tau$ then $Prob_{M \mid O}^{F}(\xrightarrow {\tau }, {\mathcal {C}}) = Prob_{N \mid O}^{F'}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}}, {\mathcal {C}})$.

  Indeed, if $P,Q \in {\mathcal {C}}$, then, by definition of ${\mathcal {R}}$, $P \equiv \bar{P} \mid \bar{O}$, $Q \equiv \bar{Q} \mid \bar{O}$ and $\bar{P} \approx _{p}^{{\mathcal {F}}} \bar{Q}$. Then there exists ${\mathcal {D}} \in {\mathcal {N}} / \approx _{p}^{{\mathcal {F}}}$ such that ${\mathcal {D}} = \{\bar{P} : \bar{P} \mid \bar{O} \in {\mathcal {C}}\}$. Now we have three cases to consider:

  • (i) if $M \mid O \xrightarrow {\tau } \llbracket M \mid O'\rrbracket _{\theta }$ because $O \xrightarrow {\tau } \llbracket O'\rrbracket _{\theta }$ the proof is simple, because for all $\bar{M}$ in the support of $\llbracket M \mid O'\rrbracket _{\theta }$ such that $\bar{M} \in {\mathcal {C}}$, it holds $\bar{M} \equiv M \mid O''$ and, since $M \approx _{p}^{{\mathcal {F}}} N$, $N \mid O'' \in {\mathcal {C}}$ too, by definition of ${\mathcal {R}}$. By Definition 4 there exists $\bar{F} \in {\mathcal {F}}_{{\mathcal {C}}}$ such that, by applying rule (R-Par) to the reduction $O \xrightarrow {}\llbracket O'\rrbracket _{\theta }$, $N\mid O \xrightarrow {}\llbracket O' \mid N\rrbracket _{\theta } \in Exec_{N\mid O}^{\bar{F}}$. By Theorem 1 and by Definition 8 $\exists F' \in \hat{{\mathcal {F}}}_{{\mathcal {C}}}$ such that $Prob_{N\mid O}^{\bar{F}}({\mathcal {C}}) = Prob_{N \mid O}^{F'}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}}, {\mathcal {C}})$, hence we have $Prob_{M \mid O}^{F}(\xrightarrow {\tau }, {\mathcal {C}}) = Prob_{N \mid O}^{F'}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}}, {\mathcal {C}})$ as required.

  • (ii) If $M \mid O \xrightarrow {\tau } \llbracket M' \mid O\rrbracket _{\theta }$ because $M \xrightarrow {\tau } \llbracket M'\rrbracket _{\theta }$, then by Definition 8 there exists $F_{1} \in \hat{{\mathcal {F}}}_{{\mathcal {C}}}$ such that $Prob_{M \mid O}^{F}(\xrightarrow {\tau }, {\mathcal {C}}) = Prob_{M}^{F_{1}}(\xrightarrow {\tau },{\mathcal {D}})$. Since $M \approx _{p}^{{\mathcal {F}}} N$, there exists $F_{2} \in \hat{{\mathcal {F}}}_{{\mathcal {C}}}$ such that $Prob_{M}^{F_{1}}(\xrightarrow {\tau }, {\mathcal {D}}) = Prob_{N}^{F_{2}}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}}, {\mathcal {D}})$. For each $N \xrightarrow {\tau }_{\theta _{1}} \cdots \xrightarrow {\tau }_{\theta _{k}} N_{k} \in Exec_{N}^{F_{1}}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}}, {\mathcal {D}}),$ there exists a scheduler $\bar{F} \in {\mathcal {F}}_{{\mathcal {C}}}$ such that $N \xrightarrow {}_{\theta _{1}} N_{1} \cdots \xrightarrow {}_{\theta _{k}} N_{k} \in Exec_{N}^{\bar{F}}.$ By Definition 4, since ${\mathcal {F}}_{{\mathcal {C}}}$ captures the interactions of N with any context, $\exists \bar{F'} \in {\mathcal {F}}_{{\mathcal {C}}}$ such that, by applying rule (R-Par) to each step in e: $N \mid O \xrightarrow {}_{\theta _{1}} \cdots \xrightarrow {}_{\theta _{k}} N_{k} \mid O \in Exec_{N \mid O}^{\bar{F'}}.$ By Definition 8 we finally get $F' \in \hat{{\mathcal {F}}}_{{\mathcal {C}}}$ such that:

    $$\begin{aligned}&Prob_{N}^{F_{2}}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}}, {\mathcal {D}}) = Prob_{N}^{\bar{F}}({\mathcal {D}}) \\&\quad = Prob_{N\mid O}^{\bar{F}'}({\mathcal {C}})= Prob_{N \mid O}^{F'}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}}, {\mathcal {C}}). \end{aligned}$$

  • (iii) If $M \mid O \xrightarrow {\tau } \llbracket M' \mid O'\rrbracket _{\varDelta }$ due to a synchronization between M and O, then there are two cases to consider. If $M \xrightarrow {c_{L}!\tilde{v}[l,r]} \llbracket M'\rrbracket _{\varDelta }$ and $O \xrightarrow {c?\tilde{v}@k} \llbracket O'\rrbracket _{\varDelta }$, for some tuple $\tilde{v}$ of messages, channel c, locations l, k and radius r, such that $d(l,k) \le r$, we can apply rule (Obs) obtaining $M \xrightarrow {c!\tilde{v}@K \triangleleft R} \llbracket M'\rrbracket _{\varDelta }$ for some set $R = \{l' \mid d(l,l') \le r\}$ with $k \in R$ and $K = L \cap R$.

    Hence, by Definition 8, there exists $F_{1} \in \hat{{\mathcal {F}}}_{{\mathcal {C}}}$ such that $Prob_{M \mid O}^{F}(\xrightarrow {\tau }, {\mathcal {C}}) = Prob_{M}^{F_{1}}(\xrightarrow {c!\tilde{v}@K \triangleleft R}, {\mathcal {D}}).$ Moreover, since $N \approx _{p}^{{\mathcal {F}}} M$, there exists $F_{2} \in \hat{{\mathcal {F}}}_{{\mathcal {C}}}$ such that $Prob_{M}^{F_{1}}(\xrightarrow {c!\tilde{v}@K \triangleleft R}, {\mathcal {D}}) = Prob_{N}^{F_{2}}(\mathrel {\mathop {\Longrightarrow }\limits ^{{c!\tilde{v}@K \triangleleft R}}}, {\mathcal {D}}),$ where each execution $e\in Exec_{N}^{F_{2}}(\mathrel {\mathop {\Longrightarrow }\limits ^{{c!\tilde{v}@K \triangleleft R}}}, {\mathcal {D}})$ has the form

    $$\begin{aligned} e= & {} N \xrightarrow {\tau }_{\theta _{1}} N_{1}\xrightarrow {\tau }_{\theta _2} \ldots N_{i-1}\\&\quad \xrightarrow {c!\tilde{v}@K \triangleleft R}_{\varDelta } N_{i}\xrightarrow {\tau }_{\theta _{i+1}} \ldots \ N'\,, \end{aligned}$$

    with $k \in R$, and, by applying rule (Obs) backwardly, $N_{i-1} \xrightarrow {c!\tilde{v}[l',r']}_{\varDelta } N_{i}$ for some $l'$ and $r'$ such that $d(l',k) \le r'$. We can apply rule (Bcast) obtaining $N_{i-1}\mid O \xrightarrow {c!\tilde{v}[l',r']}_{\varDelta } N_{i}\mid O'$ without changing the probability. Finally if we take $F' \in LSched$ which applies rule (Lose) to the output action, we obtain the required result:

    $$\begin{aligned} Prob_{N}^{F_{2}}\left( \mathrel {\mathop {\Longrightarrow }\limits ^{{c!\tilde{v}@K \triangleleft R}}}, {\mathcal {D}}\right) = Prob_{N \mid O}^{F'}\left( \mathrel {\mathop {\Longrightarrow }\limits ^{{ }}}, {\mathcal {C}}\right) . \end{aligned}$$

    We have finally to prove that $F' \in \hat{{\mathcal {F}}}_{{\mathcal {C}}}$. We start by the consideration that, by Definition 1, for any execution of the form $\mathrel {\mathop {\Longrightarrow }\limits ^{{\alpha }}}$ in $\hat{{\mathcal {F}}}_{{\mathcal {C}}}$, where $\alpha$ is a silent or an output action there exists a correspondent reduction in ${\mathcal {F}}_{{\mathcal {C}}}$. Since by Definition 4, for any context, there exists a scheduler in ${\mathcal {F}}_{{\mathcal {C}}}$ mimicking the behaviour exhibited by N when interacting with the given context, we can affirm that $\exists \bar{F} \in {\mathcal {F}}_{{\mathcal {C}}}$ such that $Exec_{N \mid O}^{\bar{F}}$ contains all the reductions corresponding to the executions of $Exec_{N \mid O}^{F'}$. Hence, by Definition 8, $F' \in \hat{{\mathcal {F}}}_{{\mathcal {C}}}$, as required. If $M \xrightarrow {c?\tilde{v}@k} \llbracket M'\rrbracket _{\varDelta }$ and $O \xrightarrow {c_{L}!\tilde{v}[l,r]} \llbracket O'\rrbracket _{\varDelta }$, for some message $\tilde{v}$, channel c, locations l, k and radius r, such that $d(l,k) \le r$, then by Definition 8 $\exists F_{1} \in \hat{{\mathcal {F}}}_{{\mathcal {C}}}$ such that:

    $$\begin{aligned} Prob_{M \mid O}^{F}\left( \xrightarrow {\tau }, {\mathcal {C}}\right) = Prob_{M}^{F_{1}}\left( \xrightarrow {c?\tilde{v}@k}, {\mathcal {D}}\right) , \end{aligned}$$

    and, since $M \approx _{p}^{{\mathcal {F}}} N$, there exists $F_{2} \in \hat{{\mathcal {F}}}_{{\mathcal {C}}}$ such that

    $Prob_{M }^{F_{1}}(\xrightarrow {c?\tilde{v}@k}, {\mathcal {D}}) = Prob_{N}^{F_{2}}(\mathrel {\mathop {\Longrightarrow }\limits ^{{c?\tilde{v}@k}}}, {\mathcal {D}})$ or

    $Prob_{M }^{F_{1}}(\xrightarrow {c?\tilde{v}@k}, {\mathcal {D}}) = Prob_{N}^{F_{2}}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}}, {\mathcal {D}}).$

    In the first case, since by hypothesis $k \in R$, also N is able to synchronize with O, for all executions in $Exec_{N}^{F_{2}}(\mathrel {\mathop {\Longrightarrow }\limits ^{{c?\tilde{v}@k}}}, {\mathcal {D}})$ of the form $e= N \xrightarrow {\tau }_{\theta _{1}} N_1 \xrightarrow {\tau }_{\theta _{2}} \ldots N_{i-1} \xrightarrow {c?\tilde{v}@k}_{\varDelta } N_{i}\xrightarrow {\tau }_{\theta _{i+1}} \ldots N'$ since by hypothesis $d(l,k)\le r$, then by applying rule (Bcast) we get $N_{i-1} \mid O \xrightarrow {c_{L}!\tilde{v}[l.r]} N_{i}\mid O'$, and there exists a matching execution: $N \mid O \xrightarrow {\tau }_{\theta _{1}} N_1 \mid O \xrightarrow {\tau }_{\theta _{2}}\ldots N_{i-1} \mid O \xrightarrow {c_{L}!\tilde{v}[l,r]}_{\varDelta } N_{i}\mid O' \xrightarrow {\tau }_{\theta _{i+1}}\ldots N'\mid O'.$

    By rule (Lose) to $N_{i-1} \mid O \xrightarrow {c_{L}!\tilde{v}[l,r]}_{\varDelta } N_{i}\mid O'$ and by Definition 4 $\exists \bar{F}' \in {\mathcal {F}}_{{\mathcal {C}}}$ such that, $Prob_{N\mid O}^{\bar{F}'}({\mathcal {C}}) = Prob_{N}^{F_{2}}({\mathcal {D}}).$ By Definition 8 $\exists F' \in \hat{{\mathcal {F}}}_{{\mathcal {C}}}$ such that, $Prob_{N\mid O}^{F'}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}}, {\mathcal {C}}) = Prob_{N \mid O}^{\bar{F}'}({\mathcal {C}}).$ If N is not able to receive the message the proof is analogous, because $\exists F' \in \hat{{\mathcal {F}}}_{{\mathcal {C}}}$ such that, for each execution in $Exec_{N}^{F_{1}}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}}, {\mathcal {D}})$ of the form $N \xrightarrow {\tau }_{\theta _{1}} N_{1} \ldots \xrightarrow {\tau }_{\theta _{k}} N_{k}$, by applying rule (Par) to each step we have that $N\mid O \xrightarrow {\tau }_{\theta _{1}} N_{1} \mid O \ldots \xrightarrow {\tau }_{\theta _{k}} N_{k} \mid O$, and by applying rule (Bcast) and (Lose) to O, and then (Par) to $N_{k} \mid O$, we get:

    $N\mid O \xrightarrow {\tau }_{\theta _{1}} N_{1} \mid O \ldots \xrightarrow {\tau }_{\theta _{k}} N_{k} \mid O \xrightarrow {\tau }_{\varDelta } N_{k} \mid O' \in Exec_{N \mid O}^{F'}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}}, {\mathcal {C}})$, hence, since the output of O does not change the probabilities of the executions, we get: $Prob_{M\mid O}^{F}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}}, {\mathcal {C}}) =\! Prob_{M}^{F_{1}}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}}, {\mathcal {D}}) = Prob_{N}^{F_{2}}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}}, {\mathcal {D}}) =\! Prob_{N \mid O}^{F'}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}}, {\mathcal {C}}).$

• 2. if $\alpha =c!\tilde{v}@K \triangleleft R$ then

  $$\begin{aligned} Prob_{M \mid O}^{F}(\xrightarrow {c!\tilde{v}@K \triangleleft R}, {\mathcal {C}}) = Prob_{N \mid O}^{F'}(\mathrel {\mathop {\Longrightarrow }\limits ^{{c!\tilde{v}@K \triangleleft R }}}, {\mathcal {C}})\,. \end{aligned}$$

  The proof is analogous to point (iii) of the previous item.

• 3. if $\alpha =c?\tilde{v}@k$ then it holds

  $$\begin{aligned} Prob_{M \mid O}^{F}(\xrightarrow {\alpha }, {\mathcal {C}}) = Prob_{N \mid O}^{F'}(\mathrel {\mathop {\Longrightarrow }\limits ^{{\alpha }}}, {\mathcal {C}}) \end{aligned}$$

  or $Prob_{M \mid O}^{F}(\xrightarrow {\alpha }, {\mathcal {C}}) = Prob_{N \mid O}^{F'}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}}, {\mathcal {C}})$. If $P,Q \in {\mathcal {C}}$, then by definition of ${\mathcal {R}}$, $P \equiv \bar{P} \mid \bar{O}$, $Q \equiv \bar{Q} \mid \bar{O}$ and $\bar{P} \approx _{p}^{{\mathcal {F}}} \bar{Q}$. Hence there exists ${\mathcal {D}} \in {\mathcal {N}} / \approx _{p}^{{\mathcal {F}}}$ such that ${\mathcal {D}} = \{\bar{P} : \bar{P} \mid \bar{O} \in {\mathcal {C}}\}$. Now we have two cases to consider:

  • (i) The transition is due to an action performed by O, hence $O \xrightarrow {\alpha }_{\varDelta } O'$ and $M \mid O' \in {\mathcal {C}}$. But since $M \approx _{p}^{{\mathcal {F}}} N$, then also $N \mid O' \in {\mathcal {C}}$, and, by Definition 8 there exists $F' \in \hat{{\mathcal {F}}}_{{\mathcal {C}}}$ such that by applying rule (Par) to $O \xrightarrow {\alpha } O'$, we get $N \mid O \xrightarrow {\alpha } N \mid O'$ obtaining:

    $$\begin{aligned} Prob_{M \mid O}^{F}(\xrightarrow {\alpha }, {\mathcal {C}}) = Prob_{N \mid O}^{F'}(\mathrel {\mathop {\Longrightarrow }\limits ^{{\alpha }}}, {\mathcal {C}}). \end{aligned}$$

  • (ii) The transition is due to an action performed by M. By Definition 8 $\exists F_{1} \in \hat{{\mathcal {F}}}_{{\mathcal {C}}}$ such that $Prob_{M \mid O}^{F}(\xrightarrow {\alpha }, {\mathcal {C}}) = Prob_{M}^{F_{1}}(\xrightarrow {\alpha }, {\mathcal {D}})$. Since $M \approx _{p}^{{\mathcal {F}}} N$, there exists $F_{2} \in \hat{{\mathcal {F}}}_{{\mathcal {C}}}$ such that $Prob_{M}^{F_{1}}(\xrightarrow {\alpha }, {\mathcal {D}}) = Prob_{N}^{F_{2}}(\mathrel {\mathop {\Longrightarrow }\limits ^{{\alpha }}}, {\mathcal {D}})$, or $Prob_{M}^{F_{1}}(\xrightarrow {\alpha }, {\mathcal {D}}) = Prob_{N}^{F_{2}}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}}, {\mathcal {D}})$. In both cases, for $e \in Exec_{N}^{F_{1}}(\mathrel {\mathop {\Longrightarrow }\limits ^{{\hat{\alpha }}}}, {\mathcal {D}})$: $e = N \xrightarrow {\alpha _{1}}_{\theta _{1}} N_{1} \ldots \xrightarrow {\alpha _{k}}_{\theta _{k}} N_{k}$ by rule (Par) to each step we get:

    $N\mid O \xrightarrow {\alpha _{1}}_{\theta _{1}} N_{1} \mid O \ldots \xrightarrow {\alpha _{k}}_{\theta _{k}} N_{k}\mid O$.

    Then, we have that $\exists F' \in LSched$ such that

    $$\begin{aligned} Prob_{N}^{F_{2}}(\mathrel {\mathop {\Longrightarrow }\limits ^{{\alpha }}}, {\mathcal {D}}) = Prob_{N\mid O}^{F'}(\mathrel {\mathop {\Longrightarrow }\limits ^{{\alpha }}}, {\mathcal {C}})\,, \end{aligned}$$

    or

    $$\begin{aligned} Prob_{N}^{F_{2}}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}}, {\mathcal {D}}) = Prob_{N \mid O}^{F'}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}}, {\mathcal {C}})\,. \end{aligned}$$

    In order to prove that $F' \in \hat{{\mathcal {F}}}_{{\mathcal {C}}}$, we start by the consideration that, by Definition 8 there exists at least a context $C[\cdot ]$ and $\exists \bar{F} \in {\mathcal {F}}_{{\mathcal {C}}}$ such that $C[N] \xrightarrow {}C'[N']$, and, by the reduction rules we get:

    $$\begin{aligned} C[\cdot ] \equiv (\nu \tilde{d}) m[\bar{c}_{L,r} \langle \tilde{v} \rangle .P]_{l} \mid M_{1} \end{aligned}$$

    for some $\tilde{d}$ such that $c \not \in \tilde{d}$, some m, some set L of locations, some process P, some (possibly empty) network $M_{1}$, some location l and some radius r such that $d(l,k) \le r$. Then, by Definition 4 there exists a scheduler allowing $m[\bar{c}_{L,r} \langle \tilde{v} \rangle .P]_{l} \xrightarrow {}\llbracket m[P]_{l}\rrbracket _{\varDelta }$, and again by Definition 4 there exists a scheduler such that $m[\bar{c}_{L,r} \langle \tilde{v} \rangle .P]_{l} \mid N \mid O \xrightarrow {}^{*} \llbracket m[P]_{l} \mid N' \mid O'\rrbracket _{\varDelta }$, and hence, by Definition 8, $F' \in \hat{{\mathcal {F}}}_{\mathcal {C}}$ as required.

Case 2. Let us consider now the relation

$$\begin{aligned} {\mathcal {S}} = \{((\nu d) M, (\nu d) N ) : M \approx _{p}^{{\mathcal {F}}} N \}. \end{aligned}$$

Let ${\mathcal {C}}\in {\mathcal {N}} / {\mathcal {S}}$: if $P,Q \in {\mathcal {C}}$, then by definition of ${\mathcal {S}}$ we have $P \equiv (\nu \bar{d})\bar{P}$, $Q \equiv (\nu \bar{d})\bar{Q}$ and $\bar{P} \approx _{p}^{{\mathcal {F}}} \bar{Q}$. Hence $\exists {\mathcal {D}} \in {\mathcal {N}} / \approx _{p}^{{\mathcal {F}}}$ such that ${\mathcal {D}} = \{\bar{P} : (\nu \bar{d})\bar{P} \in {\mathcal {C}}\}$.

We have to prove that, $\forall F \in \hat{{\mathcal {F}}}_{{\mathcal {C}}}$, $\exists F' \in \hat{{\mathcal {F}}}_{{\mathcal {C}}}$ such that, $\forall {\mathcal {C}} \in {\mathcal {N}} / {\mathcal {S}}$, $\forall \alpha$:

• 1. $\alpha = \tau$ implies $Prob_{(\nu d)M}^{F}(\xrightarrow {\tau }, {\mathcal {C}}) = Prob_{(\nu d) N}^{F'}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}}, {\mathcal {C}})$. Since $\mathtt {Chan}(\tau ) = \bot$, by Definition 8 $\exists F_{1} \in \hat{{\mathcal {F}}}_{\mathcal {C}}$ such that $Prob_{(\nu d)M}^{F}(\xrightarrow {\tau }, {\mathcal {C}}) = Prob_{M}^{F_{1}}(\xrightarrow {\tau }, {\mathcal {D}})$ and, since $M \approx _{p}^{{\mathcal {F}}} N \exists F_{2} \in \hat{{\mathcal {F}}}_{\mathcal {C}}$ such that $Prob_{M}^{F_{1}}(\xrightarrow {\tau }, {\mathcal {D}}) = Prob_{N}^{F_{2}}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}}, {\mathcal {D}})$. Finally we can take $F' \in LSched$ mimicking the executions in the set $Exec_{N}^{F_{2}}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}}, {\mathcal {D}})$, when applying the restriction on N. Hence, we have

  $$\begin{aligned} Prob_{N}^{F_{2}}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}}, {\mathcal {D}}) = Prob_{(\nu d) N}^{F'}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}}, {\mathcal {C}})\,. \end{aligned}$$

  In order to prove that $F' \in \hat{{\mathcal {F}}}_{{\mathcal {C}}}$, we start by the consideration that, by Definition 4, for any context there exists a scheduler in ${\mathcal {F}}_{{\mathcal {C}}}$ mimicking the behaviour of N when interacting with the given context. Hence $\exists \bar{F} \in {\mathcal {F}}_{{\mathcal {C}}}$ such that $Exec_{(\nu d) N}^{\bar{F}}$ contains all the reductions corresponding to the executions in $Exec_{(\nu d) N}^{F'}$, i.e., by Definition 8, $F' \in \hat{{\mathcal {F}}}_{{\mathcal {C}}}$.

• 2. $\alpha = c!\tilde{v}@K \triangleleft R$. Since $\mathtt {Chan}(c!\tilde{v}@K \triangleleft R) \ne d$, by Definition 8 $\exists F_{1} \in \hat{{\mathcal {F}}}_{{\mathcal {C}}}$ with $Prob_{(\nu d)M}^{F}(\xrightarrow {\alpha }, {\mathcal {C}}) = Prob_{M}^{F_{1}}(\xrightarrow {\alpha }, {\mathcal {D}})$. Since $M \approx _{p}^{{\mathcal {F}}} N$, $\exists F_{2} \in \hat{{\mathcal {F}}}_{{\mathcal {C}}}$ such that $Prob_{M}^{F_{1}}(\xrightarrow {\alpha }, {\mathcal {D}}) = Prob_{N}^{F'}(\mathrel {\mathop {\Longrightarrow }\limits ^{{\alpha }}}, {\mathcal {D}})$. Since $\mathtt {Chan}(\alpha ) \ne d$, $\exists F' \in LSched$ with $Prob_{N}^{F_{2}}(\mathrel {\mathop {\Longrightarrow }\limits ^{{\alpha }}}, {\mathcal {D}}) = Prob_{(\nu d) N}^{F_{2}}(\mathrel {\mathop {\Longrightarrow }\limits ^{{\alpha }}}, {\mathcal {C}}).$ We now can prove that $F' \in \hat{{\mathcal {F}}}_{{\mathcal {C}}}$ as in the previous cases.

• 3. $\alpha = c?\tilde{v}@k$. Again, by $\mathtt {Chan}(c?\tilde{v}@k) \ne d$, by Definition 8 $\exists F_{1} \in \hat{{\mathcal {F}}}_{{\mathcal {C}}}$ with $Prob_{(\nu d)M}^{F}(\xrightarrow {\alpha }, {\mathcal {C}}) = Prob_{M}^{F_{1}}(\xrightarrow {\alpha }, {\mathcal {D}})$. Since $M \approx _{p}^{{\mathcal {F}}} N$, $\exists F_{2} \in \hat{{\mathcal {F}}}_{{\mathcal {C}}}$ such that $Prob_{M}^{F_{1}}(\xrightarrow {\alpha }, {\mathcal {D}}) = Prob_{N}^{F_{2}}(\mathrel {\mathop {\Longrightarrow }\limits ^{{\alpha }}}, {\mathcal {D}})$ or $Prob_{M}^{F_{1}}(\xrightarrow {\alpha }, {\mathcal {D}}) = Prob_{N}^{F_{2}}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}}, {\mathcal {D}})$, in the case that N is not able to receive $\tilde{v}$. In both cases, by rule (Res) to N, since $\mathtt {Chan}(\tau ) = \bot \text{ and } \mathtt {Chan}(c?\tilde{v}@k) \ne d$. Hence, $\exists F' \in LSched$ such that

  $$\begin{aligned} Prob_{N}^{F_{2}}(\mathrel {\mathop {\Longrightarrow }\limits ^{{\alpha }}}, {\mathcal {D}}) = Prob_{(\nu d)N}^{F'}(\mathrel {\mathop {\Longrightarrow }\limits ^{{\alpha }}}, {\mathcal {C}}) \end{aligned}$$

  or

  $$\begin{aligned} Prob_{N}^{F_{2}}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}}, {\mathcal {D}}) = Prob_{(\nu d) N}^{F'}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}}, {\mathcal {C}})\,. \end{aligned}$$

  Again, we prove that $F' \in \hat{{\mathcal {F}}}_{{\mathcal {C}}}$ as in the previous cases. $\square$

Proof of Theorem 3

In order to prove the completeness of the probabilistic labelled bisimilarity we show that the relation

$$\begin{aligned} {\mathcal {R}} = \{(M,N): M \cong _{p}^{{\mathcal {F}}}N\} \end{aligned}$$

is a probabilistic labelled bisimulation.

We have to prove that, $\forall F \in \hat{{\mathcal {F}}}_{{\mathcal {C}}} \exists F' \in \hat{{\mathcal {F}}}_{{\mathcal {C}}}$ such that, $\forall {\mathcal {C}} \in {\mathcal {N}} / {\mathcal {R}}$, $\forall \alpha$:

• if $\alpha = \tau$ then $Prob_M^F(\xrightarrow {\tau }, {\mathcal {C}}) = Prob_N^{F'}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}},{\mathcal {C}})$.

  By Theorem 1 and Definition 8 we know that $\exists \bar{F} \in {\mathcal {F}}_{{\mathcal {C}}}$ such that $Prob_{M}^{F}(\xrightarrow {\tau }, {\mathcal {C}}) = Prob_{M}^{\bar{F}}({\mathcal {C}})$. By $M \cong _{p}^{{\mathcal {F}}} N$, $\exists \bar{F}' \in {\mathcal {F}}_{{\mathcal {C}}}$ such that $Prob_{M}^{\hat{F}}({\mathcal {C}}) = Prob_{N}^{\bar{F}'}({\mathcal {C}})$. Again by Theorem 1 and by Definition 8 $\exists F' \in \hat{{\mathcal {F}}}_{{\mathcal {C}}}$ such that $Prob_{N}^{\hat{F}'}({\mathcal {C}})=Prob_{N}^{F'}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}},{\mathcal {C}} \cup \{\bar{N} \equiv N' \in {\mathcal {C}}\})$, but since $\cong _{p}^{{\mathcal {F}}}$ is closed under structural equivalence, $\forall \bar{N} \equiv N' \in {\mathcal {C}}$, $\bar{N} \in {\mathcal {C}}$, and hence:

  $Prob_{M}^{F}(\xrightarrow {\tau },{\mathcal {C}}) = Prob_{N}^{F'}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}}, {\mathcal {C}})$.

• if $\alpha = c!\tilde{v}@K \triangleleft R$ then $Prob_M^F(\xrightarrow {\alpha }, {\mathcal {C}}) = Prob_N^{F'}(\mathrel {\mathop {\Longrightarrow }\limits ^{{\alpha }}},{\mathcal {C}})$.

  First note that $Prob_M^F(\xrightarrow {c!\tilde{v}@K \triangleleft R}, {\mathcal {C}})$ is either 0 or 1.

  If $Prob_M^F(\xrightarrow {c!\tilde{v}@K \triangleleft R}, {\mathcal {C}}) = 0$ we are done, because it will be enough to take any scheduler $F' \in \hat{{\mathcal {F}}}_{{\mathcal {C}}}$ not allowing observable output actions on the channel c, and we get $Prob_M^F(\xrightarrow {c!\tilde{v}@K \triangleleft R}, {\mathcal {C}}) = Prob_N^{F'}(\mathrel {\mathop {\Longrightarrow }\limits ^{{c!\tilde{v}@K \triangleleft R}}}, {\mathcal {C}})$.

  If $Prob_M^F(\xrightarrow {c!\tilde{v}@K \triangleleft R}, {\mathcal {C}}) = 1$, by Theorem 1 and by Definition 8 $\exists \bar{F} \in {\mathcal {F}}_{{\mathcal {C}}}$ such that $M {\Downarrow }_{1}^{\bar{F}}{c@K}$, and this means that $\exists \bar{F'} \in {\mathcal {F}}_{{\mathcal {C}}}$ such that $N {\Downarrow }_{1}^{\bar{F}'}{c@K}$, hence, by Theorem 1 and by Definition 8 there exist $F' \in \hat{{\mathcal {F}}}_{{\mathcal {C}}}$ and $R'$ such that $K \subseteq R'$ and $Prob_N^{\bar{F}'}({\mathcal {C}}) = Prob_N^{F'}(\mathrel {\mathop {\Longrightarrow }\limits ^{{c!\tilde{v}@K \triangleleft R'}}}, {\mathcal {C}})$.

  We proved that $\exists R'$ with

  $$\begin{aligned} Prob_{M}^{F}(\xrightarrow {c!\tilde{v}@K \triangleleft R}, {\mathcal {C}}) = Prob_{N}^{F'}(\mathrel {\mathop {\Longrightarrow }\limits ^{{c!\tilde{v}@K \triangleleft R'}}}, {\mathcal {C}})\,, \end{aligned}$$

  now we want to show that $R' = R$. In order to mimic the effect of the action $c!\tilde{v}@K \triangleleft R$, we build the following context

  $$\begin{aligned} C[\cdot ]= & {} {\prod }_{i = 1}^{n} (n_{i}[c(\tilde{x}_{i}).[\tilde{x}_{i} = \tilde{v}]\bar{\mathtt {f}}^{(i)}_{k_{i}, r} \langle \tilde{x}_{i}\rangle ]_{k_{i}} \mid \\&\quad m_{i}[\mathtt {f}^{(i)}(\tilde{y}_{i}). {\bar{\mathtt {ok}}}^{(i)}_{k_i,r} \langle \tilde{y}_{i} \rangle ]_{k_{i}}), \end{aligned}$$

  where $R = \{k_{1}, \ldots , k_{n}\}$, $n_{i}$, $m_{i}$, $\mathtt {ok}^{(i)}$ and $\mathtt {f}^{(i)}$ are fresh $\forall i \in [1-n]$. Since $M \xrightarrow {c!\tilde{v}@K \triangleleft R}$, then the message is reachable by all nodes $n_{i}$, hence, by Definition 4 $\exists \bar{F}_{1} \in {\mathcal {F}}_{{\mathcal {C}}}$ such that $C[M] \xrightarrow {}^* \hat{M}$, where

  $$\begin{aligned} \hat{M}\equiv & {} M' \mid {\prod }_{i = 1}^{n} (n_{i}[\mathbf {0}]_{k_{i}} \mid m_{i}[\bar{\mathtt {ok}}^{(i)}_{k_i,r} \langle \tilde{v}_{i}\rangle ]_{k_{i}}\\\equiv & {} M' \mid {\prod }_{i = 1}^{n} (m_{i}[\bar{\mathtt {ok}}^{(i)}_{k_i,r} \langle \tilde{v_{i}}\rangle ]_{k_{i}}\, \end{aligned}$$

  with and , $\forall i \in [1-n]$.

  The absence of the barb on the channels $\mathtt {f}^{(i)}$ together with the presence of the barb on the channels $\mathtt {ok}^{(i)}$ ensures that all the locations in R have been able to receive the message. Since $C[M] \cong _{p}^{{\mathcal {F}}} C[N]$, $\exists \bar{F}_{2} \in {\mathcal {F}}_{{\mathcal {C}}}$ such that $Prob_{C[M]}^{\bar{F}_{1}}({\mathcal {C}}') = Prob_{C[N]}^{\bar{F}_{2}}({\mathcal {C}}')$ where $\hat{M} \in {\mathcal {C}}'$.

  Therefore, $C[N] \xrightarrow {}^* \hat{N}$ with and $\hat{N} {\Downarrow }_{1}^{\bar{F}_{2}}{\mathtt {ok}^{(i)}@R}$. The constraints on the barbs allow us to deduce that

  $$\begin{aligned} \hat{N}\equiv & {} N' \mid {\prod }_{i = 1}^{n} (n_{i}[\mathbf {0}]_{k_{i}} \mid m_{i}[\bar{\mathtt {ok}}^{(i)}_{k_i,r} \tilde{v}_{i}]_{k_{i}}) \\\equiv & {} N' \mid {\prod }_{i = 1}^{n} (m_{i}[\bar{\mathtt {ok}}^{(i)}_{k_i,r} \tilde{v}_{i}]_{k_{i}})\,, \end{aligned}$$

  which implies $N \mathrel {\mathop {\Longrightarrow }\limits ^{{c!\tilde{v}@K \triangleleft R}}} N'$, or $N \mathrel {\mathop {\Longrightarrow }\limits ^{{ }}} N'$ in case (Lose) has been applied to the output action on the channel c. Since $\hat{M}, \hat{N} \in {\mathcal {C}}$, then $\hat{M} \cong _{p}^{{\mathcal {F}}} \hat{N}$, and since $\cong _p^{{\mathcal {F}}}$ is contextual, it results $(\nu \mathtt {ok}^{(1)}\ldots \mathtt {ok}^{(n)}) \hat{M} \cong _{p}^{{\mathcal {F}}_{{\mathcal {M}}}} (\nu \mathtt {ok}^{(1)} \ldots \mathtt {ok}^{(n)}) \hat{N}$. By applying (Struct Res Par):

  $$\begin{aligned}&(\nu \mathtt {ok}^{(1)}\ldots \mathtt {ok}^{(n)}) \hat{M} \\&\quad \equiv M' \mid (\nu \mathtt {ok}^{(1)}\ldots \mathtt {ok}^{(n)})\\&\qquad {\prod }_{i = 1}^{n} (m_{i}[\bar{\mathtt {ok}}^{(i)}_{k_i,r} \langle \tilde{v_{i}}\rangle ]_{k_{i}}) \equiv M' \end{aligned}$$

  and

  $$\begin{aligned}&(\nu \mathtt {ok}^{(1)}\ldots \mathtt {ok}^{(n)}) \hat{N} \\&\quad \equiv N' \mid (\nu \mathtt {ok}^{(1)}\ldots \mathtt {ok}^{(n)}) \\&\qquad {\prod }_{i = 1}^{n} (m_{i}[\bar{\mathtt {ok}}^{(i)}_{k_i,r} \langle \tilde{v_{i}}\rangle ]_{k_{i}}) \equiv N' \end{aligned}$$

  and, since the network

  $$\begin{aligned}&(\nu \mathtt {ok}^{(1)}\ldots \mathtt {ok}^{(n)}) {\prod }_{i = 1}^{n} (m_{i}[\bar{\mathtt {ok}}^{(i)}_{k_i,r} \langle \tilde{v_{i}}\rangle ]_{k_{i}}) \end{aligned}$$

  is silent, we can derive $M' \cong _{p}^{{\mathcal {F}}} N'$. Since $N' \in {\mathcal {C}}$ and $N \mathrel {\mathop {\Longrightarrow }\limits ^{{c!\tilde{v}@K \triangleleft R}}} N'$, by Definition 8 $\exists F' \in \hat{{\mathcal {F}}}_{{\mathcal {C}}}$ such that $Prob_N^{F'}(\mathrel {\mathop {\Longrightarrow }\limits ^{{c!\tilde{v}@K \triangleleft R}}}, {\mathcal {C}})= 1 = Prob_M^{F}(\mathrel {\mathop {\Longrightarrow }\limits ^{{c!\tilde{v}@K \triangleleft R}}}, {\mathcal {C}}),$ as required.

• if $\alpha = c?\tilde{v}@k$ then $Prob_M^F(\xrightarrow {\alpha }, {\mathcal {C}}) = Prob_N^{F'}(\mathrel {\mathop {\Longrightarrow }\limits ^{{\alpha }}},{\mathcal {C}})$ or $Prob_N^{F'}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}},{\mathcal {C}})$.

  We notice that $Prob_M^F(\xrightarrow {c?\tilde{v}@k}, {\mathcal {C}})$ is either 0 or 1. If $Prob_M^F(\xrightarrow {c?\tilde{v}@k}, {\mathcal {C}}) = 0$ we are done, because it will be enough to take any scheduler $F' \in \hat{{\mathcal {F}}}_{{\mathcal {C}}}$ not allowing input actions on the channel c. Therefore we obtain that $Prob_M^F(\xrightarrow {c?\tilde{v}@k}, {\mathcal {C}}) = Prob_N^{F'}(\mathrel {\mathop {\Longrightarrow }\limits ^{{c?\tilde{v}@k}}}, {\mathcal {C}})$.

  If $Prob_M^F(\xrightarrow {c?\tilde{v}@k}, {\mathcal {C}}) = 1$, because $M \xrightarrow {c?\tilde{v}@k} \llbracket M'\rrbracket _{\varDelta }$, by Definition 4 there exists at least a context $C[\cdot ]$ and $\exists \bar{F} \in {\mathcal {F}}_{{\mathcal {C}}}$ such that $C[M] \xrightarrow {}C'[M']$, and by Theorem 1 we have $C[\cdot ] \equiv (\nu \tilde{d}) m[\bar{c}_{L,r} \langle \tilde{v} \rangle .P]_{l} \mid M_{1}$ and $C'[\cdot ] \equiv (\nu \tilde{d}) m[P]_{l} \mid M_{1}'$ for some m, some tuple $\tilde{d}$ of channels such that $c \notin \tilde{d}$, some set L of messages, some radius r, some process P, some location l such that $d(l,k) \le r$ and some (possibly empty) networks $M_{1}$ and $M_{1}'$. By Definition 4, for any context there exists a scheduler in ${\mathcal {F}}_{{\mathcal {C}}}$ allowing m to perform the output when interacting with any context. Hence we can build the following context:

  $C_{1}[\cdot ] = \cdot \mid m[\bar{c}_{L,r} \langle \tilde{v} \rangle .P]_{l} \mid m_{1}[c(\tilde{x}).\bar{\mathtt {f}}_{k,r'} \langle \tilde{x} \rangle .\bar{\mathtt {ok}}_{k,r'} \langle \tilde{x} \rangle ]_{k},$

  in order to mimic the behaviour of the networks, with m static, $\mathtt {f}$ and $\mathtt {ok}$ fresh channels, $r' >0$ and $d(l,k) > r' \forall l \in {{ Loc }} \text{ such } \text{ that } l \ne k$.

  Hence, $\exists \bar{F}_{1} \in {\mathcal {F}}_{{\mathcal {C}}}$ such that $C_{1}[M] \xrightarrow {}^{*} M' \mid m[P]_{l} \mid m_{1}[\bar{\mathtt {ok}}_{k,r'} \langle \tilde{v} \rangle ]_{k} \in Exec_{C[M]}^{\bar{F}_{1}},$

  with and .

  The reduction sequence above must be matched by a corresponding reduction sequence of the form $C_{1}[N] \xrightarrow {}^{*} N' \mid m[P]_{l} \mid m[\bar{\mathtt {ok}}_{k,r'} \langle \tilde{v} \rangle ]_{k}$, with

  

  and

  $N' \mid m[P]_{l} \mid m[\bar{\mathtt {ok}}_{k,r'} \langle \tilde{v} \rangle ]_{k} {\Downarrow }_{1}^{\hat{F}_{2}}{\mathtt {ok}@k}$ for some $\bar{F}_2 \in {\mathcal {F}}_{{\mathcal {C}}}$.

  This does not ensure that N actually performed the input action, but we can conclude that $\exists F'\in LSched$ and $N'$ such that either $N \mathrel {\mathop {\Longrightarrow }\limits ^{{c?\tilde{v}@k}}} N'$ or $N \mathrel {\mathop {\Longrightarrow }\limits ^{{ }}} N'$. Since $M' \mid m[P]_{l} \mid m[\bar{\mathtt {ok}}_{k,r'} \langle \tilde{v} \rangle ]_{k} \cong _{p} N' \mid m[P]_{l} \mid m[\bar{\mathtt {ok}}_{k,r'} \langle \tilde{v} \rangle ]_{k}$ and $\cong _{p}^{{\mathcal {F}}}$ is is a contextual relation, we can easily derive $M' \cong _{p}^{{\mathcal {F}}} N'$ (applying the rules for structural equivalence), i.e., there exists $F' \in LSched$ such that:

  $Prob_M^F(\xrightarrow {c?\tilde{v}@k}, {\mathcal {C}}) = 1= Prob_N^{F'}(\mathrel {\mathop {\Longrightarrow }\limits ^{{c?\tilde{v}@k}}}, {\mathcal {C}})$ or

  $Prob_M^F(\xrightarrow {c?\tilde{v}@k}, {\mathcal {C}}) = 1= Prob_N^{F'}(\mathrel {\mathop {\Longrightarrow }\limits ^{{ }}}, {\mathcal {C}}).$

  Now we have only to prove that $F' \in \hat{{\mathcal {F}}}_{{\mathcal {C}}}$, but this follows straightforwardly by Definition 8, since $\bar{F}_{2} \in {\mathcal {F}}_{{\mathcal {C}}}$. $\square$