1–LABEL:LastPageAug. 07, 2017Sep. 28, 2018

*An extended abstract appeared in Proc. 37th FORTE, LNCS 10321:139-155, Springer, 2017 [LMT17b].

# Equational Reasonings in Wireless Network Gossip Protocols*

Ruggero Lanottea  aDipartimento di Scienza e Alta Tecnologia, Università degli
Studi delll’Insubria, Como, Italy<EMAIL_ADDRESS><EMAIL_ADDRESS>,  Massimo Merrob  bDipartimento di Informatica,
Università degli Studi di Verona, Verona, Italy<EMAIL_ADDRESS>and
Simone Tinia

###### Abstract.

_Gossip protocols_ have been proposed as a robust and efficient method for
disseminating information throughout large-scale networks. In this paper, we
propose a compositional analysis technique to study formal probabilistic
models of gossip protocols expressed in a simple probabilistic timed process
calculus for _wireless sensor networks_. We equip the calculus with a
_simulation theory_ to compare probabilistic protocols that have similar
behaviour up to a certain tolerance. The theory is used to prove a number of
algebraic laws which revealed to be very effective to estimate the
performances of _gossip networks_ , with and without _communication
collisions_ , and _randomised gossip networks_. Our simulation theory is an
asymmetric variant of the _weak bisimulation metric_ that maintains most of
the properties of the original definition. However, our asymmetric version is
particularly suitable to reason on protocols in which the systems under
consideration are not approximately equivalent, as in the case of gossip
protocols.

###### Key words and phrases:

Wireless sensor network, gossip protocol, (bi)simulation metric, algebraic
theory

## Introduction

_Wireless sensor networks_ (WSNs) are (possibly large-scale) networks of
sensor nodes deployed in strategic areas to gather data. Sensor nodes
collaborate using wireless communications with an asymmetric many-to-one data
transfer model. Typically, they send sensed events or data, by a specific
communication protocol, to a specific node called the sink node or base
station, which collects the requested information. WSNs are primarily designed
for monitoring environments that humans cannot easily reach (_e.g._ , motion,
target tracking, fire detection, chemicals, temperature); they are also used
as embedded systems (_e.g._ , environmental monitoring, biomedical sensor
engineering, smart homes) or mobile applications (_e.g._ , when attached to
robots or vehicles). In wireless sensor networks, sensor nodes are usually
battery-powered, and the energy expenditure of sensors has to be wisely
managed by their architectures and protocols to prolong the overall network
lifetime. _Energy conservation_ is thus one of the major issues in sensor
network communications.

_Flooding_ is a traditional robust algorithm that delivers data packets in a
network from a source to a destination. In the context of WSNs, flooding means
that all nodes receiving a message propagate it to all neighbours by
broadcast. This causes unnecessary retransmissions, which increase the number
of collisions and deprive sensors of valuable battery power. Therefore,
flooding algorithms may not be suitable in the context of dense networks like
wireless sensor networks.

_Gossiping_ is an algorithm that addresses some critical problems of flooding
overhead. Basically, it is based on the repeated probabilistic exchange of
information between two members [KvS07]. The goal of gossip protocols is to
reduce the number of retransmissions by making some of the nodes discard the
message instead of forwarding it. Gossip protocols exhibit both
_nondeterministic_ and _probabilistic_ behaviour. Nondeterminism arises as
they deal with distributed networks in which the activities of individual
nodes occur nondeterministically. As to the probabilistic behaviour, nodes are
required to forward packets with a pre-specified gossip probability
$p_{\mathrm{gsp}}$. When a node receives a message, rather than immediately
retransmitting it as in flooding, it relies on the probability
$p_{\mathrm{gsp}}$ to determine whether or not to retransmit. The main benefit
is that when $p_{\mathrm{gsp}}$ is sufficiently large, the entire network
receives the broadcast message with very high probability, even though only a
subset of nodes has forwarded the message.

Most of the analyses of protocols for large-scale WSNs are usually based on
discrete-event simulators (_e.g._ , ns-2, Opnet and Glomosim). However,
different simulators often support different models of the MAC physical-layer
yielding different results, even for simple systems (see, _e.g._ , [NCO04]).
In principle, as noticed by Bakhashi et al. [BBFH07], due to their relatively
simple structure, gossip protocols lend themselves very well to formal
analysis, in order to predict their behaviour with high confidence. Formal
analysis techniques are supported by (semi-)automated tools. For instance,
_probabilistic model checking_ has been used in the context of gossip
protocols by Fehnker and Gao [FG06] and Kwiatkowska et al. [KNP08] to provide
both an exhaustive search of all possible behaviours of the system, and exact,
rather than approximate, quantitative results. Of course, a trade-off
inevitably exists. Model checking suffers from the so-called state explosion
problem, meaning that the state space of a specified system grows
exponentially with respect to its number of components. On the other hand,
simulation-based approaches are scalable to much larger and more complex
systems, at the expense of exhaustiveness and numerical accuracy.

Among the formal techniques for the analysis of complex systems, _behavioural
semantics_ , such as preorders and equivalences, provide formal instruments to
compare the behaviour of _probabilistic systems_ [JLY01, Den15]. Preorders
allow us to determine whether a system can mimic the stepwise behaviour of
another system; whereas equivalences require a sort of mutual simulation
between two systems. The most prominent examples are the _simulation preorder_
and the _bisimulation equivalence_ [LS91, SL95]. Since probability values
usually originate from observations (statistical sampling) or from
requirements (probabilistic specification), both preorders and equivalences
are only partially satisfactory as they can only say whether a system can
mimic another one. Any tiny variation of the probabilistic behaviour of a
system will break the preorder (or the equivalence) without any further
information. In practice, many system implementations can only approximate the
system specification; thus, the verification of such implementations requires
appropriate instruments to measure the quality of the approximation. To this
end, bisimulation-based _metric semantics_ [GJS90, DGJP04, vBW05, DCPP06,
dAFS09] have been successfully employed to formalise the _behavioural
distance_ between two systems.

### Contribution.

The _goal_ of this paper is to provide a compositional analysis technique to
study probabilistic models of gossip protocols in the context of WSNs. We
adopt a simple process calculus for wireless sensor networks proposed by
Lanotte and Merro [LM11] and called _Probabilistic Timed Calculus of Wireless
Systems_ (pTCWS). We then introduce the notion of _weak simulation
quasimetric_ as the asymmetric counterpart of the _weak bisimulation metric_
[DJGP02], and the quantitative analogous of the _weak simulation preorder_
[BKHH02, BHK04]. We use the definition of weak simulation quasimetric to
derive a definition of _weak simulation with tolerance_ $p\in[0,1]$, written
$\mathrel{\sqsubseteq_{p}}$, to compare probabilistic protocols; being $0$ and
$1$ the minimum and the maximum distance, respectively.

The compositionality of a behavioural semantics with respect to the parallel
operator is fundamental when reasoning on large-scale systems. We prove that
our weak simulation with tolerance matches one of the most restrictive
compositional criteria for (bi)simulation metrics, namely _non-expansiveness_
[DJGP02, DGJP04] (also known as 1-non-extensiveness [BBLM13]).

We then rely on our simulation with tolerance to develop an _algebraic theory_
for pTCWS that allows us to compose the tolerances of different sub-networks
with different behaviours. In particular, for a gossip network
$\mathrm{GSP}_{p_{\mathrm{gsp}}}$, which transmits with gossip probability
$p_{\mathrm{gsp}}$, we are able to estimate an _upper bound_ of the tolerance
$p_{\mathrm{ok}}$ needed to simulate a non-probabilistic network
$\mathrm{DONE}$ whose target nodes successfully receive the message:

$\mathrm{DONE}\>\;\sqsubseteq_{p_{\mathrm{ok}}}\;\mathrm{GSP}_{\\!p_{\mathrm{gsp}}}.$

To this end, we prove and apply a significant number of algebraic laws, whose
application can be _mechanised_ , to evaluate the performances of gossip
networks in terms of message delivery at destination. Our analysis takes into
consideration _communication collisions_ , to determine the impact of
collisions on the performance results, and investigate _randomised gossip
protocols_ , in which messages may be broadcast in different instants of time
according to some uniform distribution probability to mitigate the impact of
communication collisions.

### Outline.

In Section 1, we recall syntax and probabilistic operational semantics of
pTCWS. In Section 2, we provide the notions of weak simulation quasimetric and
weak simulation with tolerance. In Section 3, we start our analysis on
collision-free gossip protocols. In Section 4, we extend our analysis to
collision-prone gossip protocols. In Section 5, we study randomised gossip
protocols. In Section 6, we draw conclusions and discuss related and future
work.

##  1\. A probabilistic timed process calculus

$\begin{array}[]{@{\hspace*{8mm}}rcl@{\hspace*{40mm}}l@{\hspace*{6mm}}rcl@{\hspace*{7mm}}l}\lx@intercol\textit{Networks:}\hfil\lx@intercol\\\
\hskip 22.76219pt\lx@intercol\hfil M,N&\>\;::=&\boldsymbol{0}\hfil\hskip
113.81102pt&\mbox{empty network}\hfil\hskip 17.07164pt\\\\[1.0pt] \hskip
22.76219pt\lx@intercol\hfil&\quad\big{|}&{M_{1}}|{M_{2}}\hfil\hskip
113.81102pt&\mbox{parallel composition}\hfil\hskip 17.07164pt\\\\[1.0pt]
\hskip
22.76219pt\lx@intercol\hfil&\quad\big{|}&n{\boldsymbol{[}}P{\boldsymbol{]}}^{\nu}\hfil\hskip
113.81102pt&\mbox{node}\hfil\hskip 17.07164pt\\\\[1.0pt] \hskip
22.76219pt\lx@intercol\hfil&\quad\big{|}&\mathsf{Dead}\hfil\hskip
113.81102pt&\mbox{stuck network}\hfil\hskip 17.07164pt\\\\[3.0pt]
\lx@intercol\textit{Processes:}\hfil\lx@intercol\\\ \hskip
22.76219pt\lx@intercol\hfil P,Q&\>\;::=&\mathsf{nil}\hfil\hskip
113.81102pt&\mbox{termination}\hfil\hskip 17.07164pt\\\\[1.0pt] \hskip
22.76219pt\lx@intercol\hfil&\quad\big{|}&!\langle u\rangle.C\hfil\hskip
113.81102pt&\mbox{broadcast}\hfil\hskip 17.07164pt\\\\[1.0pt] \hskip
22.76219pt\lx@intercol\hfil&\quad\big{|}&\lfloor?(x){C}\rfloor D\hfil\hskip
113.81102pt&\mbox{receiver with timeout}\hfil\hskip 17.07164pt\\\\[1.0pt]
\hskip<EMAIL_ADDRESS>113.81102pt&\mbox{internal }\hfil\hskip 17.07164pt\\\\[1.0pt] \hskip
22.76219pt\lx@intercol\hfil&\quad\big{|}&\sigma{C}\hfil\hskip
113.81102pt&\mbox{sleep}\hfil\hskip 17.07164pt\\\\[1.0pt] \hskip
22.76219pt\lx@intercol\hfil&\quad\big{|}&X\hfil\hskip
113.81102pt&\mbox{process variable}\hfil\hskip 17.07164pt\\\\[1.0pt] \hskip
22.76219pt\lx@intercol\hfil&\quad\big{|}&{\mathsf{fix}}\,X.P\hfil\hskip
113.81102pt&\mbox{recursion}\hfil\hskip 17.07164pt\\\\[3.0pt]
\lx@intercol\textit{Probabilistic Choice:}\hfil\lx@intercol\\\ \hskip
22.76219pt\lx@intercol\hfil C,D&\>\;::=&\bigoplus_{i\in
I}p_{i}{:}P_{i}\hfil\hskip 113.81102pt\end{array}$

Table 1. Syntax

In Table 1, we provide the syntax of the _Probabilistic Timed Calculus of
Wireless Systems_ , pTCWS, in a two-level structure, a lower one for
_processes_ , ranged over by letters $P$, $Q$, and $R$, and an upper one for
_networks_ , ranged over by letters $M$, $N$, and $O$. We use letters
$m,n,\ldots$ for logical names, Greek symbols $\mu,\nu,\nu_{1},\ldots$ for
_sets of names_ , $x,y,z$ for _variables_ , $u$ for _values_ , and $v$ and $w$
for _closed values_ , _i.e._ , values that do not contain variables. Then, we
use $p_{i}$ for probability weights, hence $p_{i}\in[0,1]$.

A network in pTCWS is a (possibly empty) collection of nodes (which represent
devices) running in parallel and using a unique common radio channel to
communicate with each other. Nodes are also unique; _i.e._ , a node $n$ can
occur in a network only once. All nodes are assumed to have the same
transmission range (this is a quite common assumption in models for ad hoc
networks [MZS09]). The communication paradigm is _local broadcast_ ; only
nodes located in the range of the transmitter may receive data. We write
$n{\boldsymbol{[}}P{\boldsymbol{]}}^{\nu}$ for a node named $n$ (the device
network address) executing the sequential process $P$. The set $\nu$ contains
(the names of) the neighbours of $n$. Said in other words, $\nu$ contains all
nodes laying in the transmission cell of $n$ (except $n$). In this manner, we
model the network topology. Notice that the network topology could have been
represented using some kind of restriction operator à la CCS over node names;
we preferred our notation to keep at hand the neighbours of a node. Our
wireless networks have a fixed topology. Moreover, nodes cannot be created or
destroyed. Finally, we write $\mathsf{Dead}$ to denote a deadlocked network
which prevents the execution of parallel components. This is a fictitious
network which is introduced for technical convenience in the definition of our
metrics (Definition 2).

Processes are sequential and live inside the nodes. The symbol $\mathsf{nil}$
denotes terminated processes. The sender process $!\langle v\rangle.C$
broadcasts the value $v$, the continuation being $C$. The process
$\lfloor?(x){C}\rfloor D$ denotes a receiver with timeout. Intuitively, this
process either receives a value $v$ from a neighbour node in the current time
interval, and then continues as $C$ in which the variable $x$ is instantiated
with $v$, or it idles for one time unit and then continues as $D$, if there
are no senders in the neighbourhood. The process $\tau.C$ performs an internal
action and then continues as $C$. The process $\sigma.C$ models sleeping for
one time unit. In processes of the form $\sigma.D$ and $\lfloor?(x){C}\rfloor
D$ the occurrence of $D$ is said to be _time-guarded_. The process
${\mathsf{fix}}\,X.P$ denotes _time-guarded recursion_ , as all occurrences of
the process variable $X$ may only occur time-guarded in $P$.

The construct $\bigoplus_{i\in I}p_{i}{:}P_{i}$ denotes _probabilistic choice_
, where $I$ is a _finite_ , _non-empty_ set of indexes, and $p_{i}\in(0,1]$
denotes the probability to execute the process $P_{i}$, with $\sum_{i\in
I}p_{i}=1$. Notice that, as in [DvGHM08], in order to simplify the operational
semantics, probabilistic choices occur always underneath prefixing.

In processes of the form $\lfloor?(x){C}\rfloor D$ the variable $x$ is bound
in $C$. Similarly, in process ${\mathsf{fix}}\,X.P$ the process variable $X$
is bound in $P$. This gives rise to the standard notions of _free (process)
variables_ and _bound (process) variables_ and _$\alpha$ -conversion_. We
identify processes and networks up to $\alpha$-conversion. A process is said
to be _closed_ if it does not contain free (process) variables. We always work
with closed processes: the absence of free variables is trivially maintained
at run-time. We write ${\\{^{v}\\!/\\!_{x}\\}}P$ (_resp._ ,
${\\{^{v}\\!/\\!_{x}\\}}C$) for the substitution of the variable $x$ with the
value $v$ in the process $P$ (_resp._ , probabilistic choice $C$). Similarly,
we write ${\\{^{P}\\!/\\!_{X}\\}}Q$ (_resp._ , ${\\{^{P}\\!/\\!_{X}\\}}C$) for
the substitution of the process variable $X$ with the process $P$ in $Q$
(_resp._ , in $C$).

We report some _notational conventions_. With an abuse of notation, we will
write _$?(x).C$_ as an abbreviation for
${\mathsf{fix}}\,X.\lfloor?(x){C}\rfloor(1{\colon}X)$, where the process
variable $X$ does not occur in $C$. $\prod_{i\in I}M_{i}$ denotes the parallel
composition of all $M_{i}$, for $i\in I$. We identify $\prod_{i\in I}M_{i}$
with $\boldsymbol{0}$, if $I=\emptyset$. We write $P_{1}\oplus_{p}P_{2}$ for
the probabilistic process $p{\colon}P_{1}\oplus(1{-}p){\colon}P_{2}$. We
identify $1{\colon}P$ with $P$. We write $!\langle v\rangle$ as an
abbreviation for $!\langle v\rangle.1{\colon}\mathsf{nil}$. For $k>0$ we write
$\sigma^{k}.P$ as an abbreviation for $\sigma\ldots\sigma.P$, where prefix
$\sigma$ appears $k$ times. Given a network $M$, ${\mathsf{nds}}(M)$ returns
the names of $M$. If $m\in{\mathsf{nds}}(M)$, the function $\mathsf{ngh}(m,M)$
returns the set of the neighbours of $m$ in $M$. Thus, for
$M=M_{1}|m{\boldsymbol{[}}P{\boldsymbol{]}}^{\nu}|M_{2}$ it holds that
$\mathsf{ngh}(m,M)=\nu$. We write $\mathsf{ngh}(M)$ for
$\bigcup_{m\in{\mathsf{nds}}(M)}\mathsf{ngh}(m,M)$.

[Structural congruence] _Structural congruence_ , written $\equiv$, is defined
as the smallest equivalence relation over networks, preserved by parallel
composition, which is a commutative monoid with respect to parallel
composition with neutral element $\boldsymbol{0}$, and for which
$n{\boldsymbol{[}}{\mathsf{fix}}\,X.P{\boldsymbol{]}}^{\nu}\equiv
n{\boldsymbol{[}}{\\{^{{\mathsf{fix}}\,X.P}\\!/\\!_{X}\\}}P{\boldsymbol{]}}^{\nu}$.

The syntax presented in Table 1 allows us to derive networks which are somehow
ill-formed. With the following definition we rule out networks:  (i) where
nodes can be neighbours of themselves;  (ii) with different nodes with the
same name;  (iii) with non-symmetric neighbouring relations.  Finally, in
order to guarantee clock synchronisation among nodes, we require network
connectivity. [Well-formedness] A network $M$ is said to be _well-formed_ if

  * •

whenever $M\equiv M_{1}\mid m{\boldsymbol{[}}P_{1}{\boldsymbol{]}}^{\nu}$ it
holds that $m\not\in\nu$;

  * •

whenever $M\equiv M_{1}\mid
m_{1}{\boldsymbol{[}}P_{1}{\boldsymbol{]}}^{\nu_{1}}\mid
m_{2}{\boldsymbol{[}}P_{2}{\boldsymbol{]}}^{\nu_{2}}$ it holds that $m_{1}\neq
m_{2}$;

  * •

whenever $M\equiv N\mid
m_{1}{\boldsymbol{[}}P_{1}{\boldsymbol{]}}^{\nu_{1}}\mid
m_{2}{\boldsymbol{[}}P_{2}{\boldsymbol{]}}^{\nu_{2}}$ we have
$m_{1}\in\nu_{2}$ iff $m_{2}\in\nu_{1}$;

  * •

for all $m,n\in{\mathsf{nds}}(M)$ there are
$m_{1},\ldots,m_{k}\in{\mathsf{nds}}(M)$, such that $m=m_{1}$, $n=m_{k}$, and
$m_{i}\in\mathsf{ngh}({m_{i{+}1}},M)$ for $1\leq i\leq k{-}1$.

Henceforth, we will always work with well-formed networks.

###  1.1. Probabilistic labelled transition semantics

Along the lines of [DvGHM08], we propose an _operational semantics_ for pTCWS
associating with each network a graph-like structure representing its possible
evolutions: we use a generalisation of labelled transition systems that
includes probabilities. Below, we report the necessary mathematical machinery.
A (discrete) _probability sub-distribution_ over a set $S$ is a function
$\Delta\colon S\to[0,1]$ with $\sum_{s\in S}\Delta(s)\in(0,1]$. We denote
$\sum_{s\in S}\Delta(s)$ by $\mid\\!\\!{\Delta}\\!\\!\mid$. The _support_ of a
probability sub-distribution $\Delta$ is given by $\lceil\Delta\rceil=\\{s\in
S:\Delta(s)>0\\}$. We write ${\mathcal{D}}_{\mathrm{sub}}(S)$, ranged over by
$\Delta$, $\Theta$, $\Phi$, for the set of all finite-support probability sub-
distributions over $S$. A probability sub-distribution
$\Delta\in{\mathcal{D}}_{\mathrm{sub}}(S)$ is said to be a _probability
distribution_ if $\mid\\!\\!{\Delta}\\!\\!\mid=1$. With ${\mathcal{D}}(S)$ we
denote the set of all probability distributions over $S$ with finite support.
For any $s\in S$, the _point (Dirac) distribution at $s$_, denoted
$\overline{s}$, assigns probability $1$ to $s$ and $0$ to all others elements
of $S$, so that $\lceil\overline{s}\rceil=\\{s\\}$.

Let $I$ be a finite index such that (i) $\Delta_{i}$ is a sub-distribution in
${\mathcal{D}}_{\mathrm{sub}}(S)$ for each $i\in I$, and (ii) $p_{i}\geq 0$
are probabilities such that $\sum_{i\in I}p_{i}\in(0,1]$. Then, the
probability sub-distribution $\sum_{i\in
I}p_{i}\cdot\Delta_{i}\in{\mathcal{D}}_{\mathrm{sub}}(S)$ is defined as
$(\sum_{i\in
I}p_{i}\cdot\Delta_{i})(s)\,\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}\;\,\sum_{i\in
I}p_{i}\cdot\Delta_{i}(s)$, for all $s\in S$. We write a sub-distribution as
$p_{1}\cdot\Delta_{1}+\ldots+p_{n}\cdot\Delta_{n}$ when the index set $I$ is
$\\{1,\ldots,n\\}$. In the following, we will often write $\sum_{i\in
I}p_{i}\Delta_{i}$ instead of $\sum_{i\in I}p_{i}\cdot\Delta_{i}$. Definition
1 and Definition 1 generalise to sub-distributions in
${\mathcal{D}}_{\mathrm{sub}}(\texttt{pTCWS})$. Given two probability sub-
distributions $\Delta$ and $\Theta$, we write $\Delta\equiv\Theta$ if
$\Delta([M]_{\equiv})=\Theta([M]_{\equiv})$ for all equivalence classes
$[M]_{\equiv}\subseteq\texttt{pTCWS}$ of $\equiv$. Moreover, a probability
sub-distribution $\Delta\in{\mathcal{D}}_{\mathrm{sub}}(\texttt{pTCWS})$ is
said to be well-formed if its support contains only well-formed networks.

We follow the standard probabilistic generalisation of labelled transition
systems [Seg95]. [Probabilistic LTS] A _probabilistic labelled transition
system_ (pLTS) is a triple $\langle S,{\mathcal{L}},\rightarrow\rangle$ where
(i) $S$is a set of states;  (ii) ${\mathcal{L}}$is a set of transition labels;
(iii) $\rightarrow$is a labelled transition relation contained in
$S\times{\mathcal{L}}\times\mathcal{D}(S)$.  The operational semantics of
pTCWS is given by a particular pLTS
$\langle\texttt{pTCWS},{\mathcal{L}},\rightarrow\rangle$, where
${\mathcal{L}}=\\{m!v{\triangleright}\mu,$ $m?v,$ $\tau,\sigma\\}$ contains
the labels to denote broadcasting, reception, internal actions and time
passing, respectively. The definition of the relations
$\xrightarrow{\,{\lambda}\,}$, for $\lambda\in{\mathcal{L}}$, is given by the
SOS rules in Table 2. Some of these rules use an obvious notation for
distributing parallel composition over a sub-distribution:
$({\Delta}\mid{\Theta})(M)=\Delta(M_{1})\cdot\Theta(M_{2})$ if
$M={M_{1}}|{M_{2}}$; $({\Delta}\mid{\Theta})(M)=\boldsymbol{0}$ otherwise.

Furthermore, the definition of the labelled transition relation relies on a
semantic interpretation of (nodes containing) probabilistic processes in terms
of probability distributions.

For any probabilistic choice $\bigoplus_{i\in I}p_{i}{\colon}P_{i}$ over a
finite index set $I$, we write $\llbracket n{\boldsymbol{[}}\bigoplus_{i\in
I}p_{i}{\colon}P_{i}{\boldsymbol{]}}^{\mu}\rrbracket$ to denote the
probability distribution $\sum_{i\in
I}p_{i}\cdot\overline{n{\boldsymbol{[}}P_{i}{\boldsymbol{]}}^{\mu}}$.

$\begin{array}[]{l@{\hspace*{4mm}}l}{\mbox{\small(Snd)}}\>\;\begin{array}[]{c}-\\\
\hline\cr m{\boldsymbol{[}}!\langle
v\rangle.C{\boldsymbol{]}}^{\nu}\xrightarrow{\,{m!v\vartriangleright\nu}\,}\llbracket
m{\boldsymbol{[}}C{\boldsymbol{]}}^{\nu}\rrbracket\end{array}\hfil\hskip
11.38109pt&{\mbox{\small(Rcv)}}\>\;\begin{array}[]{c}m\in\nu\\\ \hline\cr
n{\boldsymbol{[}}\lfloor?(x){C}\rfloor
D{\boldsymbol{]}}^{\nu}\xrightarrow{\,{m?v}\,}\llbracket
n{\boldsymbol{[}}{\\{^{v}\\!/\\!_{x}\\}}C{\boldsymbol{]}}^{\nu}\rrbracket\end{array}\\\\[15.0pt]
{\mbox{\small(Rcv-$\boldsymbol{0}$)}}\>\;\begin{array}[]{c}-\\\
\hline\cr\boldsymbol{0}\xrightarrow{\,{m?v}\,}\overline{\boldsymbol{0}}\end{array}\hfil\hskip
11.38109pt&{\mbox{\small(RcvEnb)}}\>\;\begin{array}[]{c}\neg(m\in\nu\>\wedge\>{\mathsf{rcv}}(P))\quad\wedge\quad
m\neq n\\\ \hline\cr
n{\boldsymbol{[}}P{\boldsymbol{]}}^{\nu}\xrightarrow{\,{m?v}\,}\overline{n{\boldsymbol{[}}P{\boldsymbol{]}}^{\nu}}\end{array}\\\\[15.0pt]
{\mbox{\small(RcvPar)}}\>\;\begin{array}[]{c}M\xrightarrow{\,{m?v}\,}\Delta\quad\quad
N\xrightarrow{\,{m?v}\,}\Theta\\\ \hline\cr M\mid
N\xrightarrow{\,{m?v}\,}\Delta|\Theta\end{array}\hfil\hskip
11.38109pt&{\mbox{\small(Bcast)}}\>\;\begin{array}[]{c}M\xrightarrow{\,{m!v\vartriangleright\nu}\,}\Delta\quad
N\xrightarrow{\,{m?v}\,}\Theta\quad{\scriptstyle{\mu{:=}\nu\setminus{\mathsf{nds}}(N)}}\\\
\hline\cr M\mid
N\xrightarrow{\,{m!v\vartriangleright\mu}\,}\Delta|\Theta\end{array}\\\\[15.0pt]
{\mbox{\small(Tau)}}\>\;\begin{array}[]{c}-\\\
\hline\cr{m{\boldsymbol{[}}\tau.C{\boldsymbol{]}}^{\nu}}\xrightarrow{\,{\tau}\,}\llbracket
m{\boldsymbol{[}}C{\boldsymbol{]}}^{\nu}\rrbracket\end{array}\hfil\hskip
11.38109pt&{\mbox{\small(TauPar)}}\>\;\begin{array}[]{c}M\xrightarrow{\,{\tau}\,}\Delta\quad
N\not\equiv\mathsf{Dead}|N^{\prime}\\\ \hline\cr
M|N\xrightarrow{\,{\tau}\,}\Delta|\overline{N}\end{array}\\\\[15.0pt]
{\mbox{\small($\sigma$-$\boldsymbol{0}$)}}\>\;\begin{array}[]{c}-\\\
\hline\cr\boldsymbol{0}\xrightarrow{\,{\sigma}\,}\overline{\boldsymbol{0}}\end{array}\hfil\hskip
11.38109pt&{\mbox{\small(Timeout)}}\>\;\begin{array}[]{c}-\\\ \hline\cr
n{\boldsymbol{[}}{\lfloor?(x){C}\rfloor
D}{\boldsymbol{]}}^{\nu}\xrightarrow{\,{\sigma}\,}\llbracket
n{\boldsymbol{[}}D{\boldsymbol{]}}^{\nu}\rrbracket\end{array}\\\\[15.0pt]
{\mbox{\small($\sigma$-nil)}}\>\;\begin{array}[]{c}-\\\ \hline\cr
n{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu}\xrightarrow{\,{\sigma}\,}\overline{n{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu}}\end{array}\hfil\hskip
11.38109pt&{\mbox{\small(Sleep)}}\>\;\begin{array}[]{c}-\\\ \hline\cr
n{\boldsymbol{[}}\sigma.C{\boldsymbol{]}}^{\nu}\xrightarrow{\,{\sigma}\,}\llbracket
n{\boldsymbol{[}}C{\boldsymbol{]}}^{\nu}\rrbracket\end{array}\\\\[15.0pt]
{\mbox{\small($\sigma$-Par)}}\>\;\begin{array}[]{c}M\xrightarrow{\,{\sigma}\,}\Delta\quad\quad
N\xrightarrow{\,{\sigma}\,}\Theta\\\ \hline\cr
M|N\xrightarrow{\,{\sigma}\,}\Delta|\Theta\end{array}\hfil\hskip
11.38109pt&{\mbox{\small(Rec)}}\>\;\begin{array}[]{c}n{\boldsymbol{[}}{\\{^{{\mathsf{fix}}\,X.P}\\!/\\!_{X}\\}}P{\boldsymbol{]}}^{\nu}\xrightarrow{\,{\lambda}\,}\Delta\\\
\hline\cr
n{\boldsymbol{[}}{\mathsf{fix}}\,X.P{\boldsymbol{]}}^{\nu}\xrightarrow{\,{\lambda}\,}\Delta\end{array}\end{array}$
Table 2. Probabilistic Labelled Transition System

Let us comment on the rules of Table 2. In rule (Snd) a node $m$ broadcasts a
message $v$ to its neighbours $\nu$, the continuation being the probability
distribution associated to $m{\boldsymbol{[}}C{\boldsymbol{]}}^{\nu}$. In the
label $m!v{\triangleright}\nu$ the set $\nu$ denotes the neighbours of $m$:
all nodes in $\nu$ that are currently listening will receive the message $v$.
In rule (Rcv) a node $n$ gets a message $v$ from a neighbour node $m$, the
continuation being the probability distribution associated to
$n{\boldsymbol{[}}{\\{^{v}\\!/\\!_{x}\\}}C{\boldsymbol{]}}^{\nu}$. If no
message is received in the current time interval then the node $n$ will
continue according to $D$, as specified in rule (Timeout). Rules
(Rcv-$\boldsymbol{0}$) and (RcvEnb) serve to model reception enabling for
synchronisation purposes. For instance, rule (RcvEnb) regards nodes $n$ which
are not involved in transmissions originating from $m$. This may happen either
because the two nodes are out of range (_i.e._ , $m\not\in\nu$) or because $n$
is not willing to receive (${\mathsf{rcv}}(P)$ is a boolean predicate that
returns true if $n{\boldsymbol{[}}P{\boldsymbol{]}}^{\nu}\equiv
n{\boldsymbol{[}}\lfloor?(x){C}\rfloor D{\boldsymbol{]}}^{\nu}$, for some $x$,
$C$, $D$). In both cases, node $n$ is not affected by the transmission. In
rule (RcvPar) we model the composition of two networks receiving the same
message from the same transmitter. Rule (Bcast) models the propagation of
messages on the broadcast channel. Note that we lose track of those
transmitter’s neighbours that are in $N$. Rule (Tau) models internal
computations in a single node. The rule (TauPar) propagates internal
computations on parallel components different from the $\mathsf{Dead}$
network. Rules ($\sigma$-nil) and ($\sigma$-$\boldsymbol{0}$) are
straightforward as both terms $\boldsymbol{0}$ and
$n{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu}$ do not prevent time-
passing. Rule (Sleep) models sleeping for one time unit. Rule ($\sigma$-Par)
models time synchronisation between parallel components (we recall that
receiver processes can timeout only if there are no senders in their
neighbourhood). Rule (Rec) is standard. For rules (Bcast) and (TauPar) we
assume their symmetric counterparts. Finally, note that the semantics of the
network $\mathsf{Dead}$ is different from that of $\boldsymbol{0}$:
$\mathsf{Dead}$ does not perform any action and it prevents the evolution of
any parallel component.

####  1.1.1. Extensional labelled transition semantics

Our focus is on weak similarities, which abstract away non-observable actions,
_i.e._ , those actions that cannot be detected by a parallel network. The
adjective _extensional_ is used to stress that here we focus on those
activities that require a contribution of the environment. To this end, we
extend Table 2 by the following two rules:

${\mbox{\small(ShhSnd)}}\>\;\begin{array}[]{c}M\xrightarrow{\,{m!v{\triangleright}\emptyset}\,}\Delta\\\
\hline\cr
M\xrightarrow{\,{\tau}\,}\Delta\end{array}\quad\quad\quad\quad\quad{\mbox{\small(ObsSnd)}}\>\;\begin{array}[]{c}M\xrightarrow{\,{m!v{\triangleright}\nu}\,}\Delta\quad\nu\neq\emptyset\\\
\hline\cr{M}\xrightarrow{\,{!v{\triangleright}\nu}\,}{\Delta}\end{array}$

Rule (ShhSnd) models transmissions that cannot be observed because there is no
potential receiver outside the network $M$. Rule (ObsSnd) models transmissions
that may be observed by those nodes of the environment contained in $\nu$.
Notice that the name of the transmitter is removed from the label. This is
motivated by the fact that receiver nodes do not have a direct manner to
observe the identity of the transmitter. On the other hand, a network $M$
performing the action $m?v$ can be observed by an external node $m$ which
transmits the value $v$ to an appropriate set of nodes in $M$. Notice that the
action $!v{\triangleright}\nu$ does not propagate over parallel components
(there is no rule for that). As a consequence, the rule (ObsSnd) can only be
applied to the whole network, never in a sub-network.

In the rest of the paper, the metavariable $\alpha$ will range over the
following four kinds of actions: $!v{\triangleright}\nu$, $m?v$, $\sigma$,
$\tau$. They denote anonymous broadcast to specific nodes, message reception,
time passing, and internal activities, respectively.

Finally, having defined the labelled transitions that can be performed by a
network, we can easily concatenate these transitions to define the possible
computation traces of a network. A _computation trace_ for a network $M$ is a
sequence of steps of the form
$M_{1}\xrightarrow{\,{\alpha_{1}}\,}\dots\xrightarrow{\,{\alpha_{n-1}}\,}M_{n}$
where for any $i$, with $1\leq i\leq n-1$, we have
$M_{i}\xrightarrow{\,{\alpha_{i}}\,}\Delta_{i+1}$ such that
$M_{i+1}\in\lceil\Delta_{i+1}\rceil$.

###  1.2. Time properties

The calculus pTCWS enjoys a number of desirable time properties [LM11] that
will be very useful for our purposes.

Proposition 1 formalises the deterministic nature of time passing: a network
can reach at most one new distribution by executing the action $\sigma$.

######  Proposition 1 (Time Determinism).

Let $M$ be a well-formed network. If $M\xrightarrow{\,{\sigma}\,}\Delta$ and
$M\xrightarrow{\,{\sigma}\,}\Theta$ then $\Delta$ and $\Theta$ are the same.

The maximal progress property says that sender nodes transmit immediately.
Said in other words, the passage of time cannot block transmissions.

######  Proposition 2 (Maximal Progress).

Let $M$ be a well-formed network. If either $M\equiv m{\boldsymbol{[}}!\langle
v\rangle.C{\boldsymbol{]}}^{\nu}|N$ or $M\equiv
m{\boldsymbol{[}}\tau.C{\boldsymbol{]}}^{\nu}|N$ then
$M\xrightarrow{\,{\sigma}\,}\Delta$ for no distribution $\Delta$.

Patience guarantees that a process will wait indefinitely until it can
communicate [HR95]. In our setting, this means that if neither transmissions
nor internal actions can fire then it must be possible to execute a
$\sigma$-action to let time pass.

######  Proposition 3 (Patience).

Let $M=\prod_{i\in I}{m_{i}{\boldsymbol{[}}P_{i}{\boldsymbol{]}}^{\nu_{i}}}$
be a well-formed network such that for all $i\in I$ it holds that
${P_{i}}\neq{!\langle v\rangle.C}$ and $P_{i}\neq\tau.C$, then there is a
distribution $\Delta$ s.t. $M\xrightarrow{\,{\sigma}\,}\Delta$.

Finally, our networks satisfy the _well-timedness_ (or _finite variability_)
property [NS92]. Intuitively, only a finite number of instantaneous actions
can fire between two contiguous $\sigma$-actions. In pTCWS, this property
holds because recursion is defined to be time-guarded.

######  Proposition 4 (Well-Timedness).

For any well-formed network $M$ there is an upper bound $k\in\mathbb{N}$ such
that whenever
$M\mathrel{\;\raisebox{0.0pt}{$\stackrel{{\scriptstyle\,\alpha_{1}}}{{\makebox[14.14459pt]{\rule{0.0pt}{4.30554pt}\mbox{}\leavevmode\xleaders\hbox{$\mkern-2.6mu\relbar\mkern-2.6mu$}\hfill\mbox{}}}}$}\rightarrow}\\!\cdots\\!\mathrel{\;\raisebox{0.0pt}{$\stackrel{{\scriptstyle\,\alpha_{h}}}{{\makebox[14.44922pt]{\rule{0.0pt}{4.30554pt}\mbox{}\leavevmode\xleaders\hbox{$\mkern-2.6mu\relbar\mkern-2.6mu$}\hfill\mbox{}}}}$}\rightarrow}N$,
with $\alpha_{j}\not\in\\{m?v,\sigma\\}$ for $1\leq j\leq h$, then $h\leq k$.

##  2\. Weak simulation with tolerance

In this section, we introduce _weak simulation quasimetrics_ as an instrument
to derive a notion of approximate simulation between networks. Our goal is to
define a family of relations $\mathrel{\sqsubseteq_{p}}$ over networks, with
$p\in[0,1]$, to formalise the concept of _simulation with a tolerance $p$_.
Intuitively, we wish to write $M\mathrel{\sqsubseteq_{p}}N$ if $N$ can
simulate $M$ with a tolerance $p$. Thus, $\mathrel{\sqsubseteq_{0}}$ should
coincide with the standard weak probabilistic simulation [BKHH02, BHK04],
whereas $\mathrel{\sqsubseteq_{1}}$ should be equal to
$\texttt{pTCWS}{}\times\texttt{pTCWS}$.

In a probabilistic setting, the definition of weak transition is somewhat
complicated by the fact that (strong) transitions take processes (in our case
networks) to distributions; consequently if we are to use weak transitions
$\ext@arrow 0359\Rightarrowfill@{}{\,{\hat{\alpha}}\,}$ which abstract away
from non-observable actions then we need to generalise transitions, so that
they take (sub-)distributions to (sub-)distributions.

For a network $M$ and a distribution $\Delta$, we write
$M\xrightarrow{\,{\hat{\tau}}\,}\Delta$ if either
$M\xrightarrow{\,{\tau}\,}\Delta$ or $\Delta=\overline{M}$. Then, for
$\alpha\neq\tau$, we write $M\xrightarrow{\,{\hat{\alpha}}\,}\Delta$ if
$M\xrightarrow{\,{\alpha}\,}\Delta$. Relation
$\xrightarrow{\,{\hat{\alpha}}\,}$ is extended to model transitions from sub-
distributions to sub-distributions. For a sub-distribution $\Delta=\sum_{i\in
I}p_{i}\overline{M_{i}}$, we write
$\Delta\xrightarrow{\,{\hat{\alpha}}\,}\Theta$ if there is a non-empty set
$J\subseteq I$ such that $M_{j}\xrightarrow{\,{\hat{\alpha}}\,}\Theta_{j}$ for
all $j\in J$,
$M_{i}\mathrel{{\xrightarrow{\,{\hat{\alpha}}\,}}\makebox[0.0pt][r]{$\not$\hskip
8.61108pt}}{\\!}$, for all $i\in I\setminus J$, and $\Theta=\sum_{j\in
J}p_{j}\Theta_{j}$. Note that if $\alpha\neq\tau$ then this definition admits
that only some networks in the support of $\Delta$ make the
$\xrightarrow{\,{\hat{\alpha}}\,}$ transition. Then, we define the weak
transition relation $\ext@arrow 0359\Rightarrowfill@{}{\,{\hat{\tau}}\,}$ as
the transitive and reflexive closure of $\xrightarrow{\,{\hat{\tau}}\,}$,
_i.e._ , $\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\tau}}\,}=(\xrightarrow{\,{\hat{\tau}}\,})^{\ast}$,
while for $\alpha\neq\tau$ we let $\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\alpha}}\,}$ denote $\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\tau}}\,}\xrightarrow{\,{\hat{\alpha}}\,}\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\tau}}\,}$.

Assume a node $n{\boldsymbol{[}}\tau.({!\langle
v_{1}\rangle}\oplus_{\frac{1}{3}}{!\langle
v_{2}\rangle}){\boldsymbol{]}}^{\nu}$ that broadcasts $v_{1}$ with probability
$\frac{1}{3}$, and $v_{2}$ with probability $\frac{2}{3}$. By an application
of rule (Tau) we derive the transition

$n{\boldsymbol{[}}\tau.({!\langle v_{1}\rangle}\oplus_{\frac{1}{3}}{!\langle
v_{2}\rangle}){\boldsymbol{]}}^{\nu}\;\mathrel{\;\raisebox{0.0pt}{$\stackrel{{\scriptstyle\,\tau}}{{\makebox[10.72676pt]{\rule{0.0pt}{4.30554pt}\mbox{}\leavevmode\xleaders\hbox{$\mkern-2.6mu\relbar\mkern-2.6mu$}\hfill\mbox{}}}}$}\rightarrow}\>\;\frac{1}{3}\cdot\overline{n{\boldsymbol{[}}{!\langle
v_{1}\rangle}{\boldsymbol{]}}^{\nu}}+\frac{2}{3}\cdot\overline{n{\boldsymbol{[}}!\langle
v_{2}\rangle{\boldsymbol{]}}^{\nu}}.$

Then, by an application of rule (Snd) we can derive:

  * •

either $n{\boldsymbol{[}}\tau.({!\langle
v_{1}\rangle}\oplus_{\frac{1}{3}}{!\langle
v_{2}\rangle}){\boldsymbol{]}}^{\nu}\ext@arrow
0359\Rightarrowfill@{}{\,{\widehat{n!{v_{1}}\vartriangleright\nu}}\,}\frac{1}{3}\cdot\overline{n{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu}}$,
because $n{\boldsymbol{[}}{!\langle
v_{1}\rangle}{\boldsymbol{]}}^{\nu}\mathrel{\;\raisebox{0.0pt}{$\stackrel{{\scriptstyle\,n!{v_{1}}\vartriangleright\nu}}{{\makebox[28.35931pt]{\rule{0.0pt}{4.30554pt}\mbox{}\leavevmode\xleaders\hbox{$\mkern-2.6mu\relbar\mkern-2.6mu$}\hfill\mbox{}}}}$}\rightarrow}n{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu}$

  * •

or $n{\boldsymbol{[}}\tau.({!\langle
v_{1}\rangle}\oplus_{\frac{1}{3}}{!\langle
v_{2}\rangle}){\boldsymbol{]}}^{\nu}\ext@arrow
0359\Rightarrowfill@{}{\,{\widehat{n!{v_{2}}\vartriangleright\nu}}\,}\frac{2}{3}\cdot\overline{n{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu}}$,
because $n{\boldsymbol{[}}{!\langle
v_{2}\rangle}{\boldsymbol{]}}^{\nu}\mathrel{\;\raisebox{0.0pt}{$\stackrel{{\scriptstyle\,n!{v_{2}}\vartriangleright\nu}}{{\makebox[28.35931pt]{\rule{0.0pt}{4.30554pt}\mbox{}\leavevmode\xleaders\hbox{$\mkern-2.6mu\relbar\mkern-2.6mu$}\hfill\mbox{}}}}$}\rightarrow}n{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu}$.

In order to define our notion of simulation with tolerance, we adapt the
concept of _weak bisimulation metric_ of Desharnais et al.’s [DJGP02]. In that
paper the behavioural distance between systems is measured by means of
suitable _pseudometrics_ , namely symmetric functions assigning a numeric
value to any pair of systems. Here, we consider asymmetric variants of
pseudometrics, called _pseudoquasimetrics_ , measuring the tolerance of the
_simulation_ between networks.

[Pseudoquasimetric] A function
$d\colon\texttt{pTCWS}{}\times\texttt{pTCWS}{}\to[0,1]$ is a _1-bounded
pseudoquasimetric_ over pTCWS if

  * •

$d(M,M)=0$ for all $M\in\texttt{pTCWS}{}$, and

  * •

$d(M,N)\leq d(M,O)+d(O,N)$ for all $M,N,O\in\texttt{pTCWS}{}$ (triangle
inequality).

Weak simulation quasimetrics provide the quantitative analogous of the weak
simulation game: a networks $M$ is simulated by a network $N$ with tolerance
$p$ if each transition $M\xrightarrow{\,{\alpha}\,}\Delta$ is mimicked by a
transition $N\ext@arrow 0359\Rightarrowfill@{}{\,{\hat{\alpha}}\,}\Theta$ such
that the distribution $\Delta$ is simulated by the distribution $\Theta$ with
a tolerance $q$, with $q\leq p$. As the derivative of a transition is a
probability distribution we have to lift the notion of pseudometric from pTCWS
to distributions over pTCWS. In [DJGP02], this lifting is realised by means of
linear programs, relying on the symmetry of pseudometrics. Since
pseudoquasimetrics are not symmetric, we need a different technique. Thus, to
this end, we adopt the notions of matching [Vil08] (also known as _coupling_)
and Kantorovich lifting [DD09].

[Matching] A _matching_ for a pair of distributions
$(\Delta,\Theta)\in{\mathcal{D}}(\texttt{pTCWS}{})\times{\mathcal{D}}(\texttt{pTCWS}{})$
is a distribution $\omega$ in the network product space
${\mathcal{D}}(\texttt{pTCWS}{}\times\texttt{pTCWS}{})$ such that:

  * •

$\sum_{N\in\texttt{pTCWS}{}}\omega(M,N)=\Delta(M)$, for all
$M\in\texttt{pTCWS}{}$, and

  * •

$\sum_{M\in\texttt{pTCWS}{}}\omega(M,N)=\Theta(N)$, for all
$N\in\texttt{pTCWS}{}$.

We write $\Omega(\Delta,\Theta)$ to denote the set of all matchings for
$(\Delta,\Theta)$. A matching for $(\Delta,\Theta)$ may be understood as a
transportation schedule for the shipment of probability mass from $\Delta$ to
$\Theta$ [Vil08].

[Kantorovich lifting] Let
$d\colon\texttt{pTCWS}{}\times\texttt{pTCWS}{}\to[0,1]$ be a
pseudoquasimetric. The _Kantorovich lifting_ of $d$ is the function
$\operatorname{\mathbf{K}}(d)\colon{\mathcal{D}}(\texttt{pTCWS}{})\times{\mathcal{D}}(\texttt{pTCWS}{})\to[0,1]$
defined as:

$\operatorname{\mathbf{K}}(d)(\Delta,\Theta)\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}\;\min_{\omega\in\Omega(\Delta,\Theta)}\sum_{M,N\in\texttt{pTCWS}}\omega(M,N)\cdot
d(M,N).$

Note that since we are considering only distributions with finite support, the
minimum over the set of matchings $\Omega(\Delta,\Theta)$ is well defined.

[Weak simulation quasimetric] We say that a pseudoquasimetric
$d\colon\texttt{pTCWS}{}\times\texttt{pTCWS}{}\to[0,1]$ is a _weak simulation
quasimetric_ if for all networks $M,N\in\texttt{pTCWS}$, with $d(M,N)<1$,
whenever $M\xrightarrow{\,{\alpha}\,}\Delta$ there is a distribution $\Theta$
such that $N\ext@arrow 0359\Rightarrowfill@{}{\,{\hat{\alpha}}\,}\Theta$ and
$\operatorname{\mathbf{K}}(d)(\Delta\>,\>\Theta+(1{-}\mid\\!\\!{\Theta}\\!\\!\mid)\overline{\mathsf{Dead}})\leq
d(M,N)$. In the previous definition, if $\mid\\!\\!{\Theta}\\!\\!\mid<1$ then,
with probability $1-\mid\\!\\!{\Theta}\\!\\!\mid$, there is no way to simulate
the behaviour of any network in the support of $\Delta$ (the special network
$\mathsf{Dead}$ does not perform any action).

As expected, the kernel of a weak simulation quasimetric is a _weak
probabilistic simulation_ defined along the lines of [DD11] in terms of the
notion of matching. A relation
${\mathcal{R}}\subseteq\texttt{pTCWS}{}\times\texttt{pTCWS}{}$ is a weak
probabilistic simulation iff whenever $M\,{\mathcal{R}}\,N$ and
$M\xrightarrow{\,{\alpha}\,}\Delta$ there exist a transition $N\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\alpha}}\,}\Theta$ and a matching
$\omega\in\Omega(\Delta,\Theta)$ with $\omega(M^{\prime},N^{\prime})>0$ such
that $M^{\prime}\,{\mathcal{R}}\,N^{\prime}$.

######  Proposition 5.

Let $d$ be a weak simulation quasimetric. The relation $\\{(M,N)\colon
d(M,N)=0\\}\subseteq\texttt{pTCWS}{}\times\texttt{pTCWS}{}$ is a weak
probabilistic simulation.

A crucial result in our construction process is the existence of the minimal
weak simulation quasimetric, which can be viewed as the asymmetric counterpart
of the minimal weak bisimulation metric [DJGP02].

######  Theorem 6.

There exists a weak simulation quasimetric $\operatorname{{\bf d}}$ such that
$\operatorname{{\bf d}}(M,N)\leq d(M,N)$ for all weak simulation quasimetrics
$d$ and all networks $M,N\in\texttt{pTCWS}{}$.

Now, we have all ingredients to define our simulation with tolerance $p$.
[Weak simulation with tolerance] Let $p\in[0,1]$, we say that _$N$ simulates
$M$ with tolerance $p$_, written $M\sqsubseteq_{p}N$, iff $\operatorname{{\bf
d}}(M,N)\leq p$. We write $M\simeq_{p}N$ if both $M\mathrel{\sqsubseteq_{p}}N$
and $N\mathrel{\sqsubseteq_{p}}M$.

Since the minimum weak simulation quasimetric $\operatorname{{\bf d}}$
satisfies the triangle inequality, our simulation relation is trivially
transitive in an additive sense:

######  Proposition 7 (Transitivity).

$M\mathrel{\sqsubseteq_{p}}N$ and $N\mathrel{\sqsubseteq_{q}}O$ imply
$M\mathrel{\sqsubseteq_{r}}O$, with $r{=}\min(1,p{+}q)$.

As expected, if $M\ext@arrow 0359\Rightarrowfill@{}{\,{\hat{\tau}}\,}\Delta$
then $M$ can simulate all networks in $\lceil\Delta\rceil$.

######  Proposition 8.

If $M\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\tau}}\,}(1{-}q)\overline{N}+q\Delta$, for some
$\Delta\in{\mathcal{D}}(\texttt{pTCWS}{})$, then
$N\mathrel{\sqsubseteq_{q}}M$.

Clearly the transitivity property is quite useful when doing algebraic
reasoning. However, we can derive a better tolerance when concatenating two
simulations, if one of them is derived by an application of Proposition 8.

######  Proposition 9.

If $M\mathrel{\sqsubseteq_{p}}N$ and $O\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\tau}}\,}(1-q)\overline{N}+q\Delta$, for some
$\Delta\in{\mathcal{D}}(\texttt{pTCWS}{})$, then
$M\mathrel{\sqsubseteq_{p(1-q)+q}}O$.

Intuitively, in the simulation between $M$ and $N$ the tolerance $p$ must be
weighted by taking into consideration that $O$ may evolve into $N$ with a
probability $(1-q)$.

The previous results can be generalised to the case where Proposition 8 is
applied to networks that are reached after one $\sigma$-transition.

######  Proposition 10.

Let $M$, $N$ and $O$ be networks in pTCWS such that: (i)
$M\mathrel{\sqsubseteq_{p}}N$; (ii) $N$ can only perform a transition of the
form $N\xrightarrow{\,{\sigma}\,}\overline{N^{\prime}}$, for some $N^{\prime}$
such that
$N^{\prime}\mathrel{{\xrightarrow{\,{\tau}\,}}\makebox[0.0pt][r]{$\not$\hskip
8.61108pt}}{\\!}$; (iii)
$O\xrightarrow{\,{\sigma}\,}\overline{O^{\prime}}\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\tau}}\,}(1-q)\overline{N^{\prime}}+q\Delta$,
for some $O^{\prime}\in\texttt{pTCWS}{}$ and
$\Delta\in{\mathcal{D}}(\texttt{pTCWS}{})$. Then,
$M\;\mathrel{\sqsubseteq_{p(1-q)+q}}\;O$.

In order to understand the intuition behind our weak simulation with
tolerance, we report here a few simple _algebraic laws_ (recall that
$1{\colon}P=P$).

######  Proposition 11 (Simple algebraic laws).

  1. (1)

$n{\boldsymbol{[}}P{\boldsymbol{]}}^{\mu}\>\mathrel{\sqsubseteq_{1-p}}\>n{\boldsymbol{[}}\tau.(P\oplus_{p}Q){\boldsymbol{]}}^{\mu}$

  2. (2)

$n{\boldsymbol{[}}Q{\boldsymbol{]}}^{\mu}\,\mathrel{\sqsubseteq_{r}}\,n{\boldsymbol{[}}\tau.(\tau.(P\oplus_{q}Q)\oplus_{p}R){\boldsymbol{]}}^{\mu}$,
with $r=(1-p)+pq$

  3. (3)

$n{\boldsymbol{[}}\tau.(\bigoplus_{i\in I,\,j\in
J}\,(p_{i}\,q_{j}){\colon}P_{j}^{i}){\boldsymbol{]}}^{\mu}\,\mathrel{\sqsubseteq_{0}}\,n{\boldsymbol{[}}\tau.(\bigoplus_{i\in
I}p_{i}{\colon}\tau.(\bigoplus_{j\in
J}q_{j}{\colon}P^{i}_{j}){\boldsymbol{]}}^{\mu}$

  4. (4)

$n{\boldsymbol{[}}!\langle
v\rangle.\big{(}\tau.(P\oplus_{q}\tau.P)\oplus_{p}Q\big{)}{\boldsymbol{]}}^{\mu}\>\simeq_{0}\>n{\boldsymbol{[}}!\langle
v\rangle.(P\,\oplus_{p}\,\tau.Q){\boldsymbol{]}}^{\mu}$

  5. (5)

$n{\boldsymbol{[}}!\langle v\rangle.!\langle
w\rangle{\boldsymbol{]}}^{\mu}\>\mathrel{\sqsubseteq_{r}}\>n{\boldsymbol{[}}\tau.\big{(}!\langle
v\rangle.\tau.(!\langle
w\rangle\oplus_{q}P)\>\oplus_{p}\>Q\big{)}{\boldsymbol{]}}^{\mu}$, with
$r=1-pq$.

The first law is straightforward. The second law is a generalisation of the
first one where the right-hand side must resolve two probabilistic choices in
order to simulate the left-hand side. The third law is an adaptation of the
$\tau$-law $\tau.P=P$ of CCS [Mil89] in a distributed and probabilistic
setting. Similarly, the fourth law reminds a probabilistic and distributed
variant of the $\tau$-law $a.(\tau.(P+\tau.Q))+a.Q=a.(P+\tau.Q)$. The last law
gives an example of a probabilistic simulation involving sequences of actions.
Here, $pq$ is the probability that the network on the right-hand side
simulates the network on the left-hand side by transmitting both $u$ and $v$.
In fact, we have:

$n{\boldsymbol{[}}\tau.(!\langle v\rangle.\tau.(!\langle
w\rangle\oplus_{q}P)\oplus_{p}Q){\boldsymbol{]}}^{\mu}\;\xrightarrow{\,{\tau}\,}\;p\cdot\overline{n{\boldsymbol{[}}!\langle
v\rangle.\tau.(!\langle
w\rangle\oplus_{q}P){\boldsymbol{]}}^{\mu}}+(1-p)\cdot\overline{n{\boldsymbol{[}}Q{\boldsymbol{]}}^{\mu}}$

with $n{\boldsymbol{[}}!\langle v\rangle.!\langle
w\rangle{\boldsymbol{]}}^{\mu}\mathrel{\sqsubseteq_{1-q}}n{\boldsymbol{[}}!\langle
v\rangle.\tau.(!\langle w\rangle\oplus_{q}P){\boldsymbol{]}}^{\mu}$; the
result follows by an application of Proposition 9.

A crucial property of our simulation is the possibility to reason on parallel
networks in a _compositional_ manner. Thus, if
$M_{1}\mathrel{\sqsubseteq_{p_{1}}}N_{1}$ and
$M_{2}\mathrel{\sqsubseteq_{p_{2}}}N_{2}$ then $M_{1}\mid
M_{2}\mathrel{\sqsubseteq_{p}}N_{1}\mid N_{2}$ for some $p$ depending on
$p_{1}$ and $p_{2}$; the intuition being that if one fixes the maximal
tolerance $p$ between $M_{1}\mid M_{2}$ and $N_{1}\mid N_{2}$, then there are
tolerances $p_{i}$ between $M_{i}$ and $N_{i}$, $i\in\\{1,2\\}$, ensuring that
the tolerance $p$ is respected. Following this intuition, several
compositional criteria for bisimulation metrics can be found in the
literature. Here, we show that our weak simulation with tolerance matches one
of the most restrictive among those studied in [GLT16, GT18], namely _non-
expansiveness_ [DJGP02, DGJP04] (also known as 1-non-extensiveness [BBLM13])
requiring that $p\leq p_{1}+p_{2}$.

######  Theorem 12 (Non-expansiveness law).

$M_{1}\mathrel{\sqsubseteq_{p_{1}}}N_{1}$ and
$M_{2}\mathrel{\sqsubseteq_{p_{2}}}N_{2}$ entails $M_{1}\mid
M_{2}\mathrel{\sqsubseteq_{r}}N_{1}\mid N_{2}$, with $r=\min(1,p+q)$.

Another useful property is that a network can be simulated by means of a
probabilistic choice whenever it is simulated by all components.

######  Proposition 13 (Additive law).

Let $M\sqsubseteq_{s_{i}}n{\boldsymbol{[}}P_{i}{\boldsymbol{]}}^{\mu}|N$, for
all $i\in I$, with $I$ a finite index set. Then,
$M\sqsubseteq_{r}n{\boldsymbol{[}}\tau.\bigoplus_{i\in
I}p_{i}{\colon}P_{i}{\boldsymbol{]}}^{\mu}\mid N$, for $r=\sum_{i\in
I}p_{i}s_{i}$.

Finally, we report a number of algebraic laws that will be useful in the next
section, when analysing gossip protocols.

######  Proposition 14 (Further algebraic laws).

  1. (1)

$n{\boldsymbol{[}}\sigma^{k}.\mathsf{nil}{\boldsymbol{]}}^{\mu}\>\;\simeq_{0}\>\;n{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\mu}$

  2. (2)

$\prod_{i\in
I}m_{i}{\boldsymbol{[}}P_{i}{\boldsymbol{]}}^{\mu_{i}}\simeq_{r}\prod_{j\in
J}n_{j}{\boldsymbol{[}}Q_{j}{\boldsymbol{]}}^{\nu_{j}}$ entails $\prod_{i\in
I}m_{i}{\boldsymbol{[}}\sigma.P_{i}{\boldsymbol{]}}^{\mu_{i}}\simeq_{r}\prod_{j\in
J}n_{j}{\boldsymbol{[}}\sigma.Q_{j}{\boldsymbol{]}}^{\nu_{j}}$

  3. (3)

$n{\boldsymbol{[}}\lfloor?(x){C}\rfloor
D{\boldsymbol{]}}^{\mu}\;\simeq_{0}\;n{\boldsymbol{[}}\sigma.D{\boldsymbol{]}}^{\mu}$,
if nodes in $\mu$ do not send in the current time interval

  4. (4)

$n{\boldsymbol{[}}?(x).C{\boldsymbol{]}}^{\mu}\;\simeq_{0}\;n{\boldsymbol{[}}\sigma.?(x).C{\boldsymbol{]}}^{\mu}$,
if nodes in $\mu$ do not send in the current time interval

  5. (5)

$m{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\mu}|\prod_{i\in
I}n_{i}{\boldsymbol{[}}P_{i}{\boldsymbol{]}}^{\mu_{i}}\;\mathrel{\sqsubseteq_{0}}\;m{\boldsymbol{[}}\tau.(!\langle
v\rangle\oplus_{p}\mathsf{nil}){\boldsymbol{]}}^{\mu}|\prod_{i\in
I}n_{i}{\boldsymbol{[}}P_{i}{\boldsymbol{]}}^{\mu_{i}}$ if
$\mu\subseteq\bigcup_{i\in I}n_{i}$, and for all $n_{i}\in\mu$ it holds that
$P_{i}\neq\lfloor?(x){C}\rfloor D$.

Please, notice that all laws but last one hold with respect to weak
bisimilarity; the last one holds with respect to weak similarity. Intuitively:
(1) $\mathsf{nil}$does not prevent time passing;  (2) equalities are preserved
underneath $\sigma$ prefixes;  (3) receivers timeout if there are not senders
around;  (4) this law is an instance of (3) because $?(x).C$ is an
abbreviation for
${\mathsf{fix}}\,X.\lfloor?(x).C\rfloor(1{:}X)\equiv\lfloor?(x).C\rfloor(1{:}{?(x).C})=\lfloor?(x).C\rfloor({?(x).C})$
($1{:}P$ is abbreviated with $P$);  (5) broadcasting evolves silently if there
are no receivers in the neighbourhood.

##  3\. Gossiping without collisions

The baseline model for our case study is gossiping without communication
collisions, where all nodes are perfectly synchronised (relying on some clock
synchronisation algorithm for WSNs). For the sake of clarity, communication
proceeds in synchronous _rounds_ : a node can transmit or receive only one
message per round. In our implementation, rounds are separated by
$\sigma$-actions.

The processes involved in the protocol are the following:

$\mathsf{snd}\langle
u\rangle_{p_{\mathrm{g}}}\\!\\!\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}\;\\!\\!\tau.(!\langle
u\rangle\oplus_{p_{\mathrm{g}}}\mathsf{nil})\quad\quad\mathsf{fwd}_{p_{\mathrm{g}}}\\!\\!\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}\;\\!\\!{?(x).\mathsf{resnd}\langle
x\rangle_{p_{\mathrm{g}}}}\quad\quad\mathsf{resnd}\langle
u\rangle_{p_{\mathrm{g}}}\\!\\!\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}\;\\!\\!\sigma.\mathsf{snd}\langle
u\rangle_{p_{\mathrm{g}}}\,.$

A sender broadcasts with a gossip probability $p_{\mathrm{g}}$, whereas a
forwarder rebroadcasts the received value, in the subsequent round, with the
same probability.

We apply our simulation theory to develop algebraic reasonings on _message
propagation_. As an introductory example, let us consider a fragment of a
network with two sender nodes, $m_{1}$ and $m_{2}$, and two forwarder nodes,
$n_{1}$ and $n_{2}$ which are both neighbours of $m_{1}$ and $m_{2}$. Then,
assuming $\nu=\\{n_{1},n_{2}\\}$ and
$\\{m_{1},m_{2}\\}\subseteq\nu_{1}\cap\nu_{2}$, the following algebraic law
holds:

$\begin{array}[]{c}m_{1}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p_{1}}{\boldsymbol{]}}^{\nu}\>\;\big{|}\>\;m_{2}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p_{2}}{\boldsymbol{]}}^{\nu}\>\;\big{|}\>\;n_{1}{\boldsymbol{[}}\mathsf{fwd}_{q_{1}}{\boldsymbol{]}}^{\nu_{1}}\>\;\big{|}\>\;n_{2}{\boldsymbol{[}}\mathsf{fwd}_{q_{2}}{\boldsymbol{]}}^{\nu_{2}}\\\\[3.0pt]
\mathrel{{}_{r}\\!\\!\sqsupseteq}\\\\[3.0pt]
m_{1}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu}\>\;\big{|}\>\;m_{2}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu}\>\;\big{|}\>\;n_{1}{\boldsymbol{[}}\mathsf{resnd}\langle
v\rangle_{q_{1}}{\boldsymbol{]}}^{\nu_{1}}\>\;\big{|}\>\;n_{2}{\boldsymbol{[}}\mathsf{resnd}\langle
v\rangle_{q_{2}}{\boldsymbol{]}}^{\nu_{2}}\end{array}$ (1)

with tolerance $r=(1-p_{1})(1-p_{2})$. Here, the network on the left-hand-side
evolves to the Dirac distribution of the network on the right-hand-side by
performing a sequence of $\tau$-actions. Thus, the algebraic law follows by an
application of Proposition 8 being $1-r$ the probability that the message $v$
is broadcast to both forwarder nodes $n_{1}$ and $n_{2}$. To explain in detail
how the sequence of $\tau$-actions are derived, we first observe that both
senders $m_{1}$ and $m_{2}$ start with the $\tau$-action resolving the
probabilistic choice on the transmission. Thus, by an application of rule
(Tau) we can derive the transitions ${\textstyle
m_{i}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p_{i}}{\boldsymbol{]}}^{\nu}\xrightarrow{\,{\tau}\,}p_{i}\cdot\overline{m_{i}{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu}}+(1-p_{i})\cdot\overline{m_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu}}}$,
for $i\in\\{1,2\\}$, which are propagated to the whole network by means of the
rule (TauPar). At this point, when composing these two transmissions, there
are three possible cases.

  * •

With probability $p_{1}\cdot p_{2}$ both senders $m_{1}$ and $m_{2}$ decide to
broadcast (the order of transmission is not relevant). This means that with
probability $p_{1}\cdot p_{2}$ the execution of the two $\tau$-transitions
above leads to the distribution
${\textstyle\overline{m_{1}{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu}|m_{2}{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu}|n_{1}{\boldsymbol{[}}\mathsf{fwd}_{q_{1}}{\boldsymbol{]}}^{\nu_{1}}|n_{2}{\boldsymbol{[}}\mathsf{fwd}_{q_{2}}{\boldsymbol{]}}^{\nu_{2}}}}$.
Now, if we suppose that $m_{1}$ transmits first, then we have the transition:

$\begin{array}[]{c}m_{1}{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu}\;|\;m_{2}{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu}\;|\;n_{1}{\boldsymbol{[}}\mathsf{fwd}_{q_{1}}{\boldsymbol{]}}^{\nu_{1}}\;|\;n_{2}{\boldsymbol{[}}\mathsf{fwd}_{q_{2}}{\boldsymbol{]}}^{\nu_{2}}\\\\[4.0pt]
\xrightarrow{\,{\tau}\,}\\\\[4.0pt]
\overline{m_{1}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu}\;|\;m_{2}{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu}\;|\;n_{1}{\boldsymbol{[}}\mathsf{resnd}\langle
v\rangle_{q_{1}}{\boldsymbol{]}}^{\nu_{1}}\;|\;n_{2}{\boldsymbol{[}}\mathsf{resnd}\langle
v\rangle_{q_{2}}{\boldsymbol{]}}^{\nu_{2}}}.\end{array}$

When also node $m_{2}$ broadcasts its value $v$ then we will have:

$\begin{array}[]{c}m_{1}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu}\,|\,m_{2}{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu}\,|\,n_{1}{\boldsymbol{[}}\mathsf{resnd}\langle
v\rangle_{q_{1}}{\boldsymbol{]}}^{\nu_{1}}\,|\,n_{2}{\boldsymbol{[}}\mathsf{resnd}\langle
v\rangle_{q_{2}}{\boldsymbol{]}}^{\nu_{2}}\\\\[4.0pt]
\xrightarrow{\,{\tau}\,}\\\\[4.0pt]
\overline{m_{1}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu}\,|\,m_{2}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu}\,|\,n_{1}{\boldsymbol{[}}\mathsf{resnd}\langle
v\rangle_{q_{1}}{\boldsymbol{]}}^{\nu_{1}}\,|\,n_{2}{\boldsymbol{[}}\mathsf{resnd}\langle
v\rangle_{q_{2}}{\boldsymbol{]}}^{\nu_{2}}}.\end{array}$

  * •

With probability $p_{1}\cdot(1-p_{2})+(1-p_{1})\cdot p_{2}$ exactly one of the
two senders decides to broadcast. This means that the $\tau$-transitions due
to the resolution of the probabilistic choice lead either to the distribution
${\textstyle\overline{m_{1}{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu}|m_{2}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu}|n_{1}{\boldsymbol{[}}\mathsf{fwd}_{q_{1}}{\boldsymbol{]}}^{\nu_{1}}|n_{2}{\boldsymbol{[}}\mathsf{fwd}_{q_{2}}{\boldsymbol{]}}^{\nu_{2}}}}$
or to the distribution
${\textstyle\overline{m_{1}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu}|m_{2}{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu}|n_{1}{\boldsymbol{[}}\mathsf{fwd}_{q_{1}}{\boldsymbol{]}}^{\nu_{1}}|n_{2}{\boldsymbol{[}}\mathsf{fwd}_{q_{2}}{\boldsymbol{]}}^{\nu_{2}}}}$.
In the former case, _i.e._ , when $m_{1}$ transmits, we have the transition

$\begin{array}[]{c}m_{1}{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu}\,|\,m_{2}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu}\,|\,n_{1}{\boldsymbol{[}}\mathsf{resnd}\langle
v\rangle_{q_{1}}{\boldsymbol{]}}^{\nu_{1}}\,|\,n_{2}{\boldsymbol{[}}\mathsf{resnd}\langle
v\rangle_{q_{2}}{\boldsymbol{]}}^{\nu_{2}}\\\\[4.0pt]
\xrightarrow{\,{\tau}\,}\\\\[4.0pt]
\overline{m_{1}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu}\,|\,m_{2}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu}\,|\,n_{1}{\boldsymbol{[}}\mathsf{resnd}\langle
v\rangle_{q_{1}}{\boldsymbol{]}}^{\nu_{1}}\,|\,n_{2}{\boldsymbol{[}}\mathsf{resnd}\langle
v\rangle_{q_{2}}{\boldsymbol{]}}^{\nu_{2}}}\end{array}$

while in the latter case we have the transition

$\begin{array}[]{c}m_{1}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu}\,|\,m_{2}{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu}\,|\,n_{1}{\boldsymbol{[}}\mathsf{resnd}\langle
v\rangle_{q_{1}}{\boldsymbol{]}}^{\nu_{1}}\,|\,n_{2}{\boldsymbol{[}}\mathsf{resnd}\langle
v\rangle_{q_{2}}{\boldsymbol{]}}^{\nu_{2}}\\\\[4.0pt]
\xrightarrow{\,{\tau}\,}\\\\[4.0pt]
\overline{m_{1}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu}\,|\,m_{2}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu}\,|\,n_{1}{\boldsymbol{[}}\mathsf{resnd}\langle
v\rangle_{q_{1}}{\boldsymbol{]}}^{\nu_{1}}\,|\,n_{2}{\boldsymbol{[}}\mathsf{resnd}\langle
v\rangle_{q_{2}}{\boldsymbol{]}}^{\nu_{2}}}\,.\end{array}$

  * •

With probability $(1-p_{1})(1-p_{2})$ both senders decide not to transmit. In
this case, it is simply not possible to reach the desired network in which
both nodes $n_{1}$ and $n_{2}$ forward the message, as they will never receive
anything to forward.

Summarising, the network ${\textstyle m_{1}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p_{1}}{\boldsymbol{]}}^{\nu}|m_{2}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p_{2}}{\boldsymbol{]}}^{\nu}|n_{1}{\boldsymbol{[}}\mathsf{fwd}_{q_{1}}{\boldsymbol{]}}^{\nu_{1}}|n_{2}{\boldsymbol{[}}\mathsf{fwd}_{q_{2}}{\boldsymbol{]}}^{\nu_{2}}}$
has probability $1-(1-p_{1})(1-p_{2})$ to reach (the Dirac distribution of)
$m_{1}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu}|m_{2}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu}|n_{1}{\boldsymbol{[}}\mathsf{resnd}\langle
v\rangle_{q_{1}}{\boldsymbol{]}}^{\nu_{1}}|n_{2}{\boldsymbol{[}}\mathsf{resnd}\langle
v\rangle_{q_{2}}{\boldsymbol{]}}^{\nu_{2}}$ by the application of a sequence
of $\tau$-transitions. This allows us to apply Proposition 8 to derive
Equation 1.

However, Equation 1 can be generalised to an arbitrary number of senders and
forwarders, provided that parallel contexts are unable to receive messages in
the current round.

######  Theorem 15 (Message propagation).

Let $I$ and $J$ be disjoint subsets of $\mathbb{N}$. Let $M$ be a well-formed
network defined as

$M\>\equiv\>N\>\;\big{|}\>\;\prod_{i\in
I}m_{i}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p_{i}}{\boldsymbol{]}}^{\nu_{m_{i}}}\>\;\big{|}\>\;\prod_{j\in
J}n_{j}{\boldsymbol{[}}\mathsf{fwd}_{q_{j}}{\boldsymbol{]}}^{\nu_{n_{j}}}$

such that, for all $i\in I$:  (1) $\\{n_{j}:j\in
J\\}\subseteq\nu_{m_{i}}\subseteq{\mathsf{nds}}(M)$;  (2) the nodes in
$\nu_{m_{i}}\cap{\mathsf{nds}}(N)$ cannot receive in the current round.  Then,

$M\;\mathrel{{}_{r}\\!\\!\sqsupseteq}\;N\>\;\big{|}\>\;\prod_{i\in
I}m_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m_{i}}}\>\;\big{|}\>\;\prod_{j\in
J}n_{j}{\boldsymbol{[}}\mathsf{resnd}\langle
v\rangle_{q_{j}}{\boldsymbol{]}}^{\nu_{n_{j}}}$

with $r=\prod_{i\in I}(1-p_{i})$.

As an example, consider a simple gossiping network $\mathrm{GSP}_{1}$, with
gossip probability $p$, composed by two source nodes $s_{1}$ and $s_{2}$ and a
destination node $d$. The network is the following:

$\mathrm{GSP}_{1}\;\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}\;\;\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{s_{i}}}\>\;\big{|}\>\;d{\boldsymbol{[}}\mathsf{fwd}_{1}{\boldsymbol{]}}^{\nu_{d}}$

with $\nu_{s_{1}}=\nu_{s_{2}}=\\{d\\}$ and
$\nu_{d}=\\{s_{1},s_{2},\mathit{tester}\\}$, where ${\mathit{tester}}$ is a
fresh node of the observer to test successful gossiping. For simplicity, here
and in the rest of the paper, the node $\mathit{tester}$ can receive messages
but it cannot transmit.

We would like to estimate the distance between $\mathrm{GSP}_{1}$ and a
network $\mathrm{DONE}_{1}$ in which the message $v$ has been delivered to the
destination node $d$:

$\mathrm{DONE}_{1}\;\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}\;\;\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\>\;\big{|}\>\;d{\boldsymbol{[}}\mathsf{resnd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{d}}.$

By an application of Theorem 15 it follows that
$\mathrm{GSP}_{1}\mathrel{{}_{(1-p)^{2}}\\!\\!\sqsupseteq}\,\mathrm{DONE}_{1}$.
Thus, the network $\mathrm{GSP}_{1}$ succeeds in delivering the message to the
destination $d$ with probability (at least) $1-(1-p)^{2}=2p-p^{2}$.

Actually, Theorem 15 represents an effective tool to deal with message
propagation in gossip networks. However, it requires that all forwarders
$n_{j}$ should be in the neighbouring of all senders $m_{i}$ (constraint
$\\{n_{j}:j\in J\\}\subseteq\nu_{m_{i}}$), which may represent a limitation in
many cases. Consider, for example, a gossiping network $\mathrm{GSP}_{2}$,
with gossip probability $p$, composed by two source nodes $s_{1}$ and $s_{2}$,
a destination node $d$, and three intermediate nodes $n_{1}$, $n_{2}$, and
$n_{3}$:

$\mathrm{GSP}_{2}\;\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}\;\;\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{s_{i}}}\>\;\big{|}\>\;\prod_{i=1}^{3}n_{i}{\boldsymbol{[}}\mathsf{fwd}_{p}{\boldsymbol{]}}^{\nu_{n_{i}}}\>\;\big{|}\>\;d{\boldsymbol{[}}\mathsf{fwd}_{1}{\boldsymbol{]}}^{\nu_{d}}$

where $\nu_{s_{1}}=\\{n_{1}\\}$, $\nu_{s_{2}}=\\{n_{1},n_{2}\\}$,
$\nu_{n_{1}}{=}\\{s_{1},s_{2},n_{3}\\}$, $\nu_{n_{2}}{=}\\{s_{2},n_{3}\\}$,
$\nu_{n_{3}}=\\{n_{1},n_{2},d\\}$ and $\nu_{d}=\\{n_{3},\mathit{tester}\\}$.

Here, we would like to estimate the distance between $\mathrm{GSP}_{2}$, and a
network $\mathrm{DONE}_{2}$, in which the message $v$ propagated somehow up to
the destination node $d$:

$\mathrm{DONE}_{2}\;\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}\;\;\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\>\;\big{|}\>\;\prod^{3}_{i=1}n_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{n_{i}}}\>\;\big{|}\>\;d{\boldsymbol{[}}\sigma^{2}\\!.\,\mathsf{resnd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{d}}.$

Unfortunately, we cannot directly apply Theorem 15 to capture this message
propagation because node $s_{2}$, unlike $s_{1}$, can transmit to both $n_{1}$
and $n_{2}$. In this case, before applying Theorem 15, we would need a result
to _compose estimates_ of partial networks. More precisely, a result which
would allow us to take into account, in the calculation of the tolerance, both
the probability that a sender transmits and the probability that the same
sender does not transmit.

The additive law of Proposition 13 allows us to prove the following result.

######  Theorem 16 (Composing networks).

If $M\mathrel{{\xrightarrow{\,{\sigma}\,}}\makebox[0.0pt][r]{$\not$\hskip
8.61108pt}}{\\!}$ then

$N\>\;\,\big{|}\>\;\,m{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{m}}\>\;\,\big{|}\>\;\,\prod_{j\in
J}n_{j}{\boldsymbol{[}}\lfloor?(x_{j}){P_{j}}\rfloor
Q_{j}{\boldsymbol{]}}^{\nu_{n_{j}}}\mathrel{{}_{r}\\!\\!\sqsupseteq}\>M$

with $r={p}{q_{1}}+{(1{-}p}){q_{2}}$, whenever

  * •

$N\;|\;m{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m}}\;|\;\prod_{j\in
J}n_{j}{\boldsymbol{[}}{\\{^{v}\\!/\\!_{x_{j}}\\}}P_{j}{\boldsymbol{]}}^{\nu_{n_{j}}}\mathrel{{}_{q_{1}}\\!\\!\sqsupseteq}\>M$

  * •

$N\;|\;m{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m}}\;|\;\prod_{j\in
J}n_{j}{\boldsymbol{[}}\lfloor?(x_{j}){P_{j}}\rfloor
Q_{j}{\boldsymbol{]}}^{\nu_{n_{j}}}\mathrel{{}_{q_{2}}\\!\\!\sqsupseteq}\>M$

  * •

$\\{n_{j}:j\in J\\}\subseteq\nu_{m}\subseteq\\{n_{j}:j\in
J\\}\cup{\mathsf{nds}}(N)$

  * •

nodes in $\nu_{m}\cap{\mathsf{nds}}(N)$ cannot receive in the current
round.111We could generalise the result to take into account more senders at
the same time. This would not add expressiveness, it would just speed up the
reduction process.

Intuitively:  (i) in the network $N|m{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{m}}|\prod_{j\in
J}n_{j}{\boldsymbol{[}}\lfloor?(x_{j}){P_{j}}\rfloor
Q_{j}{\boldsymbol{]}}^{\nu_{n_{j}}}$ the sender $m$ has not performed yet the
$\tau$-action that resolves the probabilistic choice between broadcasting the
message $v$ or not;  (ii) in the network $\;N\
|m{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m}}|\prod_{j\in
J}n_{j}{\boldsymbol{[}}{\\{^{v}\\!/\\!_{x_{j}}\\}}P_{j}{\boldsymbol{]}}^{\nu_{n_{j}}}$
the sender $m$ has resolved the probabilistic choice deciding to broadcast the
message $v$;  (iii) finally, in the network
$N|m{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m}}|\prod_{j\in
J}n_{j}{\boldsymbol{[}}\lfloor?(x_{j}){P_{j}}\rfloor
Q_{j}{\boldsymbol{]}}^{\nu_{n_{j}}}$ the sender $m$ has resolved the
probabilistic choice deciding not to broadcast $v$.

Later on we will use the following instance of Theorem 16.

######  Corollary 17.

If $M\mathrel{{\xrightarrow{\,{}\,}}\makebox[0.0pt][r]{$\not$\hskip
8.61108pt}}{\\!}{\sigma}$ then

$N\>\;\big{|}\>\;m{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{m}}\>\;\big{|}\>\;\prod_{j\in
J}n_{j}{\boldsymbol{[}}\mathsf{fwd}_{{q}}{\boldsymbol{]}}^{\nu_{n_{j}}}\mathrel{{}_{r}\\!\\!\sqsupseteq}\>M$

with $r=pq_{1}+(1{-}p)q_{2}$, whenever:

  * •

$N\>\;\big{|}\>\;m{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m}}\>\;\big{|}\>\;\prod_{j\in
J}n_{j}{\boldsymbol{[}}\mathsf{resnd}\langle
v\rangle_{q}{\boldsymbol{]}}^{\nu_{n_{j}}}\mathrel{{}_{q_{1}}\\!\\!\sqsupseteq}\>M$

  * •

$N\>\;\big{|}\>\;m{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m}}\>\;\big{|}\>\;\prod_{j\in
J}n_{j}{\boldsymbol{[}}\mathsf{fwd}_{{q}}{\boldsymbol{]}}^{\nu_{n_{j}}}\mathrel{{}_{q_{2}}\\!\\!\sqsupseteq}\>M$

  * •

$\\{n_{j}\mid j\in J\\}\subseteq\nu_{m}\subseteq\\{n_{j}\mid j\in
J\\}\cup{\mathsf{nds}}(M)$

  * •

nodes in $\nu_{m}\cap{\mathsf{nds}}(N)$ cannot receive in the current round.

Now, we have all algebraic tools to compute an estimation of the tolerance
$r$, such that
$\mathrm{GSP}_{2}\mathrel{{}_{r}\\!\\!\sqsupseteq}\mathrm{DONE}_{2}$.
Basically, we will compute the tolerances for two partial networks and then
will use Theorem 16 to compose the two tolerances.

As a first step, we compute an estimation for the network $\mathrm{GSP}_{2}$
in which the sender $s_{2}$ _has already broadcast_ the message $v$ to its
neighbours $n_{1}$ and $n_{2}$. To this end, we derive the following chain of
similarities by applying, in sequence:  (i) Proposition 14(5) to express that
if $n_{1}$ receives the message transmitted by $s_{2}$ then the message
broadcast by $s_{1}$ gets lost;  (ii) Proposition 14(4) to formalise that in
the current round both nodes $n_{3}$ and $d$ do not receive any message
because there are no transmitters in their neighbourhood, as a consequence,
they are obliged to timeout;  (iii) Theorem 15 in which nodes $n_{1}$ and
$n_{2}$ act as senders and $n_{3}$ as a forwarder, together with Proposition
14(2) to work underneath $\sigma$ prefixes;  (iv) Proposition 14(1) to remove
$\sigma$ prefixes in both nodes $n_{1}$ and $n_{2}$;  (v) Proposition 14(4)
because in the next round there are no nodes that can transmit to $d$;  (vi)
Theorem 15 in which $n_{3}$ acts as sender and $d$ as forwarder, together with
Proposition 14(2) to work underneath $\sigma$ prefixes;  (vii) Proposition
14(1) to remove $\sigma$ prefixes in $n_{3}$.  In all steps, we have reasoned
in a compositional manner, up to common parallel components (Theorem 12). For
convenience, in the chain below we define two auxiliary networks:
$\mathrm{NET}_{a}$ and $\mathrm{NET}_{b}$.

$\begin{array}[]{rrl}&&\mathrm{GSP}_{2}(s_{1}[v]\mbox{; }s_{2}\mbox{
gossiped})\\\\[3.0pt]
&\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}&s_{1}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{s_{1}}}\;\big{|}\;s_{2}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{2}}}\;\big{|}\;\prod^{2}_{i=1}n_{i}{\boldsymbol{[}}\mathsf{resnd}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{n_{i}}}\;\big{|}\;n_{3}{\boldsymbol{[}}\mathsf{fwd}_{p}{\boldsymbol{]}}^{\nu_{n_{3}}}\;\big{|}\;d{\boldsymbol{[}}\mathsf{fwd}_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&\mathrel{{}_{0}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\;\big{|}\;\prod^{2}_{i=1}n_{i}{\boldsymbol{[}}\mathsf{resnd}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{n_{i}}}\;\big{|}\;n_{3}{\boldsymbol{[}}\mathsf{fwd}_{p}{\boldsymbol{]}}^{\nu_{n_{3}}}\;\big{|}\;d{\boldsymbol{[}}\mathsf{fwd}_{1}{\boldsymbol{]}}^{\nu_{d}}\end{array}$
$\begin{array}[]{rrl}&\mathrel{{}_{0}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\;\big{|}\;\prod^{2}_{i=1}n_{i}{\boldsymbol{[}}\sigma.\mathsf{snd}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{n_{i}}}\;\big{|}\;n_{3}{\boldsymbol{[}}\sigma.\mathsf{fwd}_{p}{\boldsymbol{]}}^{\nu_{n_{3}}}\;\big{|}\;d{\boldsymbol{[}}\sigma.\mathsf{fwd}_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}&\mathrm{NET}_{a}\\\\[3.0pt]
&\mathrel{{}_{(1-p)^{2}}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\;\big{|}\;\prod^{2}_{i=1}n_{i}{\boldsymbol{[}}\sigma.\mathsf{nil}{\boldsymbol{]}}^{\nu_{n_{i}}}\;\big{|}\;n_{3}{\boldsymbol{[}}\sigma.\mathsf{resnd}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{n_{3}}}\;\big{|}\;d{\boldsymbol{[}}\sigma.\mathsf{fwd}_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}&\mathrm{NET}_{b}\\\\[3.0pt]
&\mathrel{{}_{0}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\;\big{|}\;\prod^{2}_{i=1}n_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{n_{i}}}\;\big{|}\;n_{3}{\boldsymbol{[}}\sigma^{2}.\,\mathsf{snd}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{n_{3}}}\;\big{|}\;d{\boldsymbol{[}}\sigma\\!.\,\mathsf{fwd}_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&\mathrel{{}_{0}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\;\big{|}\;\prod^{2}_{i=1}n_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{n_{i}}}\;\big{|}\;n_{3}{\boldsymbol{[}}\sigma^{2}\\!.\,\mathsf{snd}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{n_{3}}}\;\big{|}\;d{\boldsymbol{[}}\sigma^{2}\\!.\,\mathsf{fwd}_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&\mathrel{{}_{1-p}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\;\big{|}\;\prod^{2}_{i=1}n_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{n_{i}}}\;\big{|}\;n_{3}{\boldsymbol{[}}\sigma^{2}\\!.\,\mathsf{nil}{\boldsymbol{]}}^{\nu_{n_{3}}}\;\big{|}\;d{\boldsymbol{[}}\sigma^{2}\\!.\,\mathsf{resnd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&\mathrel{{}_{0}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\;\big{|}\;\prod^{3}_{i=1}n_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{n_{i}}}\;\big{|}\;d{\boldsymbol{[}}\sigma^{3}\\!.\,\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&=&\mathrm{DONE}_{2}.\end{array}$

By transitivity (Proposition 7) we can easily derive
$\mathrm{NET}_{b}\>\mathrel{{}_{1-p}\\!\\!\sqsupseteq}\>\mathrm{DONE}_{2}$.
This allows us to apply Proposition 10, in which $M$, $N$, and $O$ are
instantiated with $\mathrm{DONE}_{2}$, $\mathrm{NET}_{b}$, and
$\mathrm{NET}_{a}$, respectively, to derive the equation
$\mathrm{NET}_{a}\,\mathrel{{}_{1-2p^{2}+p^{3}}\\!\\!\sqsupseteq}\,\mathrm{DONE}_{2}$
where the tolerance $1-2p^{2}+p^{3}$ is obtained by solving the expression
$(1-p)(1-(1-p)^{2})+(1-p)^{2}$. By transitivity on the first two steps of the
chain above, we can finally derive the equation

$\mathrm{GSP}_{2}(s_{1}[v]\mbox{; }s_{2}\mbox{
gossiped})\;\mathrel{{}_{1-2p^{2}+p^{3}}\\!\\!\sqsupseteq}\;\,\mathrm{DONE}_{2}$
(2)

Similarly, we can compute an estimation of the tolerance which allows the
network $\mathrm{GSP}_{2}$ in which the sender $s_{2}$ _did not broadcast_ the
message $v$ to its neighbours to simulate the network $\mathrm{DONE}_{2}$. To
this end, we derive the following chain of similarities by applying, in
sequence:  (i) Theorem 15;  (ii) Proposition 14(4);  (iii) Theorem 15 and
Proposition 14(2);  (iv) Proposition 14(1) and Proposition 14(4);  (v) Theorem
15 and Proposition 14(2);  (vi) Proposition 14(1) and Proposition 14(5).
Again, in all steps, we have reasoned up to common parallel components
(Theorem 12). For convenience, in the chain below we define three auxiliary
networks: $\mathrm{NET}_{c}$, $\mathrm{NET}_{d}$ and $\mathrm{NET}_{e}$.

$\begin{array}[]{rrl}&&\mathrm{GSP}_{2}(s_{1}[v]\mbox{; }s_{2}\mbox{ did not
gossip})\\\\[3.0pt]
&\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}&s_{1}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{s_{1}}}\;\big{|}\;s_{2}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{2}}}\;\big{|}\;\prod_{i=1}^{3}n_{i}{\boldsymbol{[}}\mathsf{fwd}_{p}{\boldsymbol{]}}^{\nu_{n_{i}}}\;\big{|}\;d{\boldsymbol{[}}\mathsf{fwd}_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&\mathrel{{}_{1-p}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\;\big{|}\;n_{1}{\boldsymbol{[}}\mathsf{resnd}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{n_{1}}}\;\big{|}\;\prod^{3}_{i=2}n_{i}{\boldsymbol{[}}\mathsf{fwd}_{p}{\boldsymbol{]}}^{\nu_{n_{i}}}\;\big{|}\;d{\boldsymbol{[}}\mathsf{fwd}_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}&\mathrm{NET}_{c}\\\\[3.0pt]
&\mathrel{{}_{0}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\;\big{|}\;n_{1}{\boldsymbol{[}}\sigma.\mathsf{snd}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{n_{1}}}\;\big{|}\;\prod^{3}_{i=2}n_{i}{\boldsymbol{[}}\sigma.\mathsf{fwd}_{p}{\boldsymbol{]}}^{\nu_{n_{i}}}\;\big{|}\;d{\boldsymbol{[}}\sigma.\mathsf{fwd}_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}&\mathrm{NET}_{d}\\\\[3.0pt]
&\mathrel{{}_{1-p}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\;\big{|}\;n_{1}{\boldsymbol{[}}\sigma.\mathsf{nil}{\boldsymbol{]}}^{\nu_{n_{1}}}\;\big{|}\;n_{2}{\boldsymbol{[}}\sigma.\mathsf{fwd}_{p}{\boldsymbol{]}}^{\nu_{n_{2}}}\;\big{|}\;n_{3}{\boldsymbol{[}}\sigma.\mathsf{resnd}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{n_{3}}}\;\big{|}\;d{\boldsymbol{[}}\sigma.\mathsf{fwd}_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}&\mathrm{NET}_{e}\\\\[3.0pt]
&\mathrel{{}_{0}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\;\big{|}\;n_{1}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{n_{1}}}\;\big{|}\;n_{2}{\boldsymbol{[}}\sigma^{2}\\!.\,\mathsf{fwd}_{p}{\boldsymbol{]}}^{\nu_{n_{2}}}\;\big{|}\;n_{3}{\boldsymbol{[}}\sigma^{2}\\!.\,\mathsf{snd}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{n_{3}}}\;\big{|}\;d{\boldsymbol{[}}\sigma^{2}\\!.\,\mathsf{fwd}_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&\mathrel{{}_{1-p}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\;\big{|}\;n_{1}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{n_{1}}}\;\big{|}\;n_{2}{\boldsymbol{[}}\sigma^{2}\\!.\,\mathsf{resnd}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{n_{2}}}\;\big{|}\;n_{3}{\boldsymbol{[}}\sigma^{2}\\!.\mathsf{nil}{\boldsymbol{]}}^{\nu_{n_{3}}}\;\big{|}\;d{\boldsymbol{[}}\sigma^{2}\\!.\,\mathsf{resnd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&\mathrel{{}_{0}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\;\big{|}\;\prod^{3}_{i=1}n_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{n_{i}}}\;\big{|}\;d{\boldsymbol{[}}\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&=&\mathrm{DONE}_{2}\,.\end{array}$

Then, by transitivity (Proposition 7) we can derive the equation

$\mathrm{NET}_{e}\;\mathrel{{}_{1-p}\\!\\!\sqsupseteq}\;\,\mathrm{DONE}_{2}.$

This allows us to apply Proposition 10, in which $M$, $N$, and $O$ are
instantiated with $\mathrm{DONE}_{2}$, $\mathrm{NET}_{e}$, and
$\mathrm{NET}_{d}$, respectively, to derive the equation

$\mathrm{NET}_{d}\;\mathrel{{}_{1-p^{2}}\\!\\!\sqsupseteq}\;\,\mathrm{DONE}_{2}$

where the tolerance $1-p^{2}$ is obtained by solving the expression
$(1-p)(1-(1-p))+(1-p)$. By transitivity we can easily derive:

$\mathrm{NET}_{c}\;\mathrel{{}_{1-p^{2}}\\!\\!\sqsupseteq}\;\,\mathrm{DONE}_{2}.$

This last equation can be used to apply Proposition 9, in which $M$, $N$, and
$O$ are instantiated with $\mathrm{DONE}_{2}$, $\mathrm{NET}_{c}$, and
$\mathrm{GSP}_{2}(s_{1}[v]\mbox{; }s_{2}\mbox{ did not gossip})$,
respectively, to derive:

$\mathrm{GSP}_{2}(s_{1}[v]\mbox{; }s_{2}\mbox{ did not
gossip})\;\mathrel{{}_{1-p^{3}}\\!\\!\sqsupseteq}\;\mathrm{DONE}_{2}$ (3)

where the tolerance $1-p^{3}$ is obtained by solving the expression
$(1-p)(1-(1-p^{2}))+(1-p^{2})$.

Finally, we can apply Corollary 17 to Equations 2 and 3 to derive:

$\mathrm{GSP}_{2}\>\;\mathrel{{}_{1-(3p^{3}-2p^{4})}\\!\\!\sqsupseteq}\>\;\;\mathrm{DONE}_{2}.$

Thus, the gossip network $\mathrm{GSP}_{2}$ will succeed in propagating the
messages to the destination $d$ with probability at least $3p^{3}-2p^{4}$. For
instance, with a gossip probability $p=0.8$ the destination will receive the
message with probability $0.716$, with a margin of $10\%$. For $p=0.85$ the
success probability increases to $0.798$, with a margin of $6\%$; while for
$p=0.9$ the probability to propagate the message to the destination rises to
$0.88$, with a margin of only $2\%$. As a consequence, $p=0.9$ can be
considered the threshold of our small network.222Had we had more senders we
would have estimated a better threshold.

Note that in the previous example both messages may reach the destination node
in exactly three rounds. However, more generally, we could have different
message propagation paths in the same network which might take a different
amount of time to be traversed. The algebraic theory we developed up to now
does not allow us to deal with paths of different lengths. As an example, we
would like to estimate the distance between the network

$\mathrm{GSP}_{3}\,\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}\;\,s_{1}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{s_{1}}}\>\;\big{|}\>\;s_{2}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{s_{2}}}\>\;\big{|}\>\;n{\boldsymbol{[}}\mathsf{fwd}_{p}{\boldsymbol{]}}^{\nu_{n}}\>\;\big{|}\>\;d{\boldsymbol{[}}\mathsf{fwd}_{1}{\boldsymbol{]}}^{\nu_{d}}$

with topology $\nu_{s_{1}}=\\{d\\}$, $\nu_{s_{2}}=\\{n\\}$,
$\nu_{n}{=}\\{s_{2},d\\}$ and $\nu_{d}=\\{s_{1},n,\mathit{tester}\\}$, and the
network

$\mathrm{DONE}_{3}\,\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}\;\,s_{1}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{1}}}\>\;\big{|}\>\;s_{2}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{2}}}\>\;\big{|}\>\;n{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{n}}\>\;\big{|}\>\;d{\boldsymbol{[}}\tau.(\sigma.\mathsf{snd}\langle
v\rangle_{1}\oplus_{p}\sigma^{2}.\mathsf{snd}\langle
v\rangle_{1}){\boldsymbol{]}}^{\nu_{d}}$

in which the message $v$ propagated up to the destination node $d$ following
two different paths. Thus, $d$ will probabilistically choose between
broadcasting $v$ after one or two rounds.

The following result provides the missing instrument.

######  Theorem 18 (Composing paths).

Let $M$ be a well-formed network. Then,

$M\>\;\big{|}\>\;m{\boldsymbol{[}}\tau.\bigoplus_{i\in
I}p_{i}{\colon}Q_{i}{\boldsymbol{]}}^{\nu_{m}}\>\;\mathrel{{}_{r}\\!\\!\sqsupseteq}\>\;\prod_{j\in
J}n_{j}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{n_{j}}}\;\big{|}\;d{\boldsymbol{[}}\tau.\bigoplus_{i\in
I}p_{i}{\colon}P_{i}{\boldsymbol{]}}^{\nu_{d}}$

with $r=\sum_{i\in I}p_{i}s_{i}$, whenever
$M|m{\boldsymbol{[}}Q_{i}{\boldsymbol{]}}^{\nu_{m}}\,\mathrel{{}_{s_{i}}\\!\\!\sqsupseteq}\;\prod_{j\in
J}n_{j}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{n_{j}}}|d{\boldsymbol{[}}P_{i}{\boldsymbol{]}}^{\nu_{d}}$,
for any $i\in I$.

Let us provide an estimation of the distance between $\mathrm{GSP}_{3}$ and
$\mathrm{DONE}_{3}$. As a first step, we compute an estimation of the
tolerance which allows $\mathrm{GSP}_{3}$ to simulate the first probabilistic
behaviour of $\mathrm{DONE}_{3}$ (broadcast after one round). To this end, we
derive the following chain of similarities by applying, in sequence:  (i)
Theorem 15 to model the transmission of $s_{1}$;  (ii) again Theorem 15 to
model the transmission of $s_{2}$;  (iii) Proposition 14(5) to model that the
transmission of $n$ gets lost, together with Proposition 14(2) to work
underneath $\sigma$ prefixes.  In all steps, we reason up to parallel
components (Theorem 12).

$\begin{array}[]{rrl}&&\mathrm{GSP}_{3}(s_{1}\mbox{ gossiped}\mbox{;
}s_{2}[v])\\\\[2.0pt]
&\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}&s_{1}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{s_{1}}}\;\big{|}\;s_{2}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{s_{2}}}\;\big{|}\;n{\boldsymbol{[}}\mathsf{fwd}_{p}{\boldsymbol{]}}^{\nu_{n}}\;\big{|}\;d{\boldsymbol{[}}\mathsf{fwd}_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&\mathrel{{}_{0}\\!\\!\sqsupseteq}&s_{1}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{1}}}\;\big{|}\;s_{2}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{s_{2}}}\;\big{|}\;n{\boldsymbol{[}}\mathsf{fwd}_{p}{\boldsymbol{]}}^{\nu_{n}}\;\big{|}\;d{\boldsymbol{[}}\mathsf{resnd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&\mathrel{{}_{1-p}\\!\\!\sqsupseteq}&s_{1}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{1}}}\;\big{|}\;s_{2}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{2}}}\;\big{|}\;n{\boldsymbol{[}}\mathsf{resnd}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{n}}\;\big{|}\;d{\boldsymbol{[}}\mathsf{resnd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&=&s_{1}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{1}}}\;\big{|}\;s_{2}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{2}}}\;\big{|}\;n{\boldsymbol{[}}\sigma.\mathsf{snd}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{n}}\;\big{|}\;d{\boldsymbol{[}}\sigma.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&\mathrel{{}_{0}\\!\\!\sqsupseteq}&s_{1}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{1}}}\;\big{|}\;s_{2}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{2}}}\;\big{|}\;n{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{n}}\;\big{|}\;d{\boldsymbol{[}}\sigma.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{d}}.\end{array}$

By transitivity (Proposition 7) we derive:

$\mathrm{GSP}_{3}(s_{1}\mbox{ gossiped}\mbox{;
}s_{2}[v])\;\mathrel{{}_{1-p}\\!\\!\sqsupseteq}\;\,s_{1}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{1}}}\;\big{|}\;s_{2}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{2}}}\;\big{|}\;n{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{n}}\;\big{|}\;d{\boldsymbol{[}}\sigma.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{d}}$ (4)

Then, we compute an estimation of the tolerance which allows the network
$\mathrm{GSP}_{3}$ to simulate the second probabilistic behaviour of
$\mathrm{DONE}_{3}$. To this end, we derive the following chain of
similarities by applying, in sequence:  (i) Theorem 15 to model the
transmission of $s_{2}$;  (ii) Proposition 14(4) as without transmitters the
node $d$ is obliged to timeout;  (iii) Theorem 15 as node $n$ may transmit to
$d$, working underneath a $\sigma$ prefix (Proposition 14(2));  (iv)
Proposition 14(1) to remove a $\sigma$ prefix in node $n$.  As usual, in all
steps, we reason up to parallel components (Theorem 12). For convenience, in
the chain below we define two auxiliary networks: $\mathrm{NET}_{f}$ and
$\mathrm{NET}_{g}$.

$\begin{array}[]{rrl}&&\mathrm{GSP}_{3}(s_{1}\mbox{ did not gossip}\mbox{;
}s_{2}[v])\\\\[2.0pt]
&\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}&s_{1}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{1}}}\;\big{|}\;s_{2}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{s_{2}}}\;\big{|}\;n{\boldsymbol{[}}\mathsf{fwd}_{p}{\boldsymbol{]}}^{\nu_{n}}\;\big{|}\;d{\boldsymbol{[}}\mathsf{fwd}_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&\mathrel{{}_{1-p}\\!\\!\sqsupseteq}&s_{1}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{1}}}\;\big{|}\;s_{2}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{2}}}\;\big{|}\;n{\boldsymbol{[}}\mathsf{resnd}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{n}}\;\big{|}\;d{\boldsymbol{[}}\mathsf{fwd}_{1}{\boldsymbol{]}}^{\nu_{d}}\\\
&\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}&\mathrm{NET}_{f}\\\\[3.0pt]
&\mathrel{{}_{0}\\!\\!\sqsupseteq}&s_{1}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{1}}}\;\big{|}\;s_{2}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{2}}}\;\big{|}\;n{\boldsymbol{[}}\sigma.\mathsf{snd}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{n}}\;\big{|}\;d{\boldsymbol{[}}\sigma.\mathsf{fwd}_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&\mathrel{{}_{1-p}\\!\\!\sqsupseteq}&s_{1}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{1}}}\;\big{|}\;s_{2}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{2}}}\;\big{|}\;n{\boldsymbol{[}}\sigma.\mathsf{nil}{\boldsymbol{]}}^{\nu_{n}}\;\big{|}\;d{\boldsymbol{[}}\sigma.\mathsf{resnd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&\mathrel{{}_{0}\\!\\!\sqsupseteq}&s_{1}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{1}}}\;\big{|}\;s_{2}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{2}}}\;\big{|}\;n{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{n}}\;\big{|}\;d{\boldsymbol{[}}\sigma^{2}.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[2.0pt]
&\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}&\mathrm{NET}_{g}.\end{array}$

Then, by transitivity (Proposition 7) we can derive
$\mathrm{NET}_{f}\,\mathrel{{}_{1-p}\\!\\!\sqsupseteq}\,\mathrm{NET}_{g}$.
This last equation can be used to apply Proposition 9, in which $M$, $N$, and
$O$ are instantiated with $\mathrm{NET}_{g}$, $\mathrm{NET}_{f}$, and
$\mathrm{GSP}_{3}(s_{1}\mbox{ did not gossip}\mbox{; }s_{2}[v])$,
respectively, to derive:

$\mathrm{GSP}_{3}(s_{1}\mbox{ did not gossip;
}s_{2}[v])\>\;\mathrel{{}_{1-p^{2}}\\!\\!\sqsupseteq}\>\;\,\mathrm{NET}_{g}$
(5)

where the tolerance $1-p^{2}$ is obtained by solving the expression
$(1-p)(1-(1-p))+(1-p)$.

Finally, we can apply Theorem 18 to Equations 4 and 5 to obtain:

$\mathrm{GSP}_{3}\;\mathrel{{}_{r}\\!\\!\sqsupseteq}\;\mathrm{DONE}_{3}$

with $r=p(1-p)+(1-p)(1-p^{2})$. Thus, the network $\mathrm{GSP}_{3}$ will
succeed in transmitting both messages $v$ to the destination $d$, with
probability at least $1-r$.

We conclude by observing that, in order to deal with paths of different
length, one should apply Theorem 18 to all possible paths.

##  4\. Gossiping with collisions

An important aspect of wireless communication is the presence of collisions:
if two or more stations are transmitting over the same channel during the same
round then a _communication collision_ occurs at the receiver nodes.
Collisions in wireless systems cannot be avoided, although there are protocols
to reduce their occurrences (see, for instance, the protocol IEEE 802.11
CSMA/CA).

In Section 3, we have reasoned assuming no collisions. Here, we demonstrate
that the presence of communication collisions deteriorates the performance of
gossip protocols.

The calculus pTCWS allows us to easily express communication collisions. A
receiver node experiences a collision if it is exposed to more than one
transmission in the same round; as a consequence the reception in that round
fails. We can model this behaviour by redefining the forwarder process as
follows:

$\mathsf{resndc}\langle
u\rangle_{p_{\mathrm{g}}}\\!\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}\;\\!\lfloor?(x){\mathsf{nil}}\rfloor\mathsf{snd}\langle
u\rangle_{p_{\mathrm{g}}}\quad\quad\quad\quad\mathsf{fwdc}_{p_{\mathrm{g}}}\\!\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}\;\\!{?(x).\mathsf{resndc}\langle
x\rangle_{p_{\mathrm{g}}}}\,.$

Here, the forwarder $\mathsf{fwdc}_{p_{\mathrm{g}}}$ waits for a message in
the current round. If a second message is received in the same round then the
forwarding is doomed to fail; otherwise if no other messages are received, the
process moves to next round and broadcasts the received message with the given
gossip probability. Thus, for example, the Equation 1 seen in the previous
section becomes:

$\begin{array}[]{c}m_{1}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p_{1}}{\boldsymbol{]}}^{\nu}\;\big{|}\;m_{2}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p_{2}}{\boldsymbol{]}}^{\nu}\;\big{|}\;n_{1}{\boldsymbol{[}}\mathsf{fwdc}_{q}{\boldsymbol{]}}^{\nu_{1}}\;\big{|}\;n_{2}{\boldsymbol{[}}\mathsf{fwdc}_{r}{\boldsymbol{]}}^{\nu_{2}}\\\\[3.0pt]
\mathrel{{}_{r}\\!\\!\sqsupseteq}\\\\[3.0pt] \quad
m_{1}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu}\;\big{|}\;m_{2}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu}\;\big{|}\;n_{1}{\boldsymbol{[}}\mathsf{resndc}\langle
v\rangle_{q}{\boldsymbol{]}}^{\nu_{1}}\;\big{|}\;n_{2}{\boldsymbol{[}}\mathsf{resndc}\langle
v\rangle_{r}{\boldsymbol{]}}^{\nu_{2}}\end{array}$ (6)

with a tolerance $r=1-(p_{1}(1-p_{2})+p_{2}(1-p_{1}))$ which is definitely
greater than the tolerance $(1{-}p_{1})(1{-}p_{2})$ seen in Equation 1 for the
same network in the absence of communication collisions. As expected, the
difference between the two tolerances corresponds to the probability
$p_{1}\cdot p_{2}$ that both senders $m_{1}$ and $m_{2}$ decide to transmit.
In the previous section, we argued that in the absence of collisions the first
broadcast message is received by both nodes $n_{1}$ and $n_{2}$, while the
second message is simply ignored by $n_{1}$ and $n_{2}$. However, this
situation obviously gives rise to a communication collision. More generally,
when collisions are taken into account, Theorem 15 should be reformulated as
follows:

######  Theorem 19 (Message propagation with collisions).

Let $I$ and $J$ be disjoint subsets of $\mathbb{N}$. Let $M$ be a well-formed
network defined as

$M\equiv N\>\;\big{|}\>\;\prod_{i\in
I}m_{i}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p_{i}}{\boldsymbol{]}}^{\nu_{m_{i}}}\>\;\big{|}\>\;\prod_{j\in
J}n_{j}{\boldsymbol{[}}\mathsf{fwdc}_{q_{j}}{\boldsymbol{]}}^{\nu_{n_{j}}}$

such that, for all $i\in I$:  (1) $\\{n_{j}:j\in
J\\}\subseteq\nu_{m_{i}}\subseteq{\mathsf{nds}}(M)$, and  (2) the nodes in
$\nu_{m_{i}}\cap{\mathsf{nds}}(N)$ cannot receive in the current round.  Then,

$M\;\mathrel{{}_{r}\\!\\!\sqsupseteq}\;\,N\>\;\big{|}\>\;\prod_{i\in
I}m_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m_{i}}}\>\;\big{|}\>\;\prod_{j\in
J}n_{j}{\boldsymbol{[}}\mathsf{resndc}\langle
v\rangle_{q_{j}}{\boldsymbol{]}}^{\nu_{n_{j}}}$

with $r=1-\sum_{i\in I}p_{i}\prod_{j\in I{\setminus}\\{i\\}}(1-p_{j})$.

Here, the reader may notice that the tolerance is different with respect to
that derived in Theorem 15. This is because, in the presence of collisions,
forwarders successfully receive (and forward) a value only if exactly one
sender transmits it; the forwarding fails otherwise.

As an example, consider a variant of the gossiping network $\mathrm{GSP}_{1}$
of the previous section where communication collisions are taken into account:

$\mathrm{GSP}_{4}\;\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}\;\;\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{s_{i}}}\>\;\big{|}\>\;d{\boldsymbol{[}}\mathsf{fwdc}_{1}{\boldsymbol{]}}^{\nu_{d}}.$

The corresponding network where the message has been propagated up to the
destination node is not affected by the presence of collisions. Just for
convenience, we define $\mathrm{DONE}_{4}=\mathrm{DONE}_{1}$. Since the node
$\mathit{tester}\in\nu_{d}$ cannot transmit, by an application of Theorem 19
and Proposition 14(3) it follows that:

$\mathrm{GSP}_{4}\;\mathrel{{}_{1-2p(1-p)}\\!\\!\sqsupseteq}\;\,\mathrm{DONE}_{4}.$

Thus, $\mathrm{GSP}_{4}$ succeeds in propagating the message $v$ with (at
least) probability $2p(1-p)$. In the previous section, we have seen that in
the absence of collisions, the success probability of $\mathrm{GSP_{1}}$ is
(at least) $2p-p^{2}$. Since $2p(1-p)<2p-p^{2}$, for any $p>0$, it follows
that the presence of collisions downgrades the performance of this small
network of $p^{2}$, that coincides with the probability that both senders
transmit.

Notice that, unlike Theorem 15, Theorem 16 is still valid when dealing with
communications collisions due to its general formulation. However, for
commodity, in the following we will use two instances of it.

######  Corollary 20.

If $M\mathrel{{\xrightarrow{\,{\sigma}\,}}\makebox[0.0pt][r]{$\not$\hskip
8.61108pt}}{\\!}$ then

$\begin{array}[]{c}N\>\;\big{|}\>\;m{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{m}}\>\;\big{|}\>\;\prod_{j\in
J}n_{j}{\boldsymbol{[}}\mathsf{resndc}\langle
v\rangle_{{q}}{\boldsymbol{]}}^{\nu_{n_{j}}}\mathrel{{}_{r}\\!\\!\sqsupseteq}\>M\end{array}$

with $r=ps_{1}+(1-p)s_{2}$, whenever:

  * •

$N\>\;\big{|}\>\;m{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m}}\>\;\big{|}\>\;\prod_{j\in
J}n_{j}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{n_{j}}}\mathrel{{}_{s_{1}}\\!\\!\sqsupseteq}\>M$

  * •

$N\>\;\big{|}\>\;m{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m}}\>\;\big{|}\>\;\prod_{j\in
J}n_{j}{\boldsymbol{[}}\mathsf{resndc}\langle
v\rangle_{q}{\boldsymbol{]}}^{\nu_{n_{j}}}\mathrel{{}_{s_{2}}\\!\\!\sqsupseteq}\>M$

  * •

$\\{n_{j}:j\in J\\}\subseteq\nu_{m}\subseteq\\{n_{j}:j\in
J\\}\cup{\mathsf{nds}}(M)$

  * •

nodes in $\nu_{m}\cap{\mathsf{nds}}(M)$ cannot receive in the current round.

######  Corollary 21.

If $M\mathrel{{\xrightarrow{\,{\sigma}\,}}\makebox[0.0pt][r]{$\not$\hskip
8.61108pt}}{\\!}$ then

$\begin{array}[]{c}N\>\;\big{|}\>\;m{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{m}}\>\;\big{|}\>\;\prod_{j\in
J}n_{j}{\boldsymbol{[}}\mathsf{fwdc}_{{q}}{\boldsymbol{]}}^{\nu_{n_{j}}}\mathrel{{}_{r}\\!\\!\sqsupseteq}\>M\end{array}$

with $r=ps_{1}+(1-p)s_{2}$, whenever:

  * •

$N\>\;\big{|}\>\;m{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m}}\>\;\big{|}\>\;\prod_{j\in
J}n_{j}{\boldsymbol{[}}\mathsf{resndc}\langle
v\rangle_{q}{\boldsymbol{]}}^{\nu_{n_{j}}}\mathrel{{}_{s_{1}}\\!\\!\sqsupseteq}\>M$

  * •

$N\>\;\big{|}\>\;m{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m}}\>\;\big{|}\>\;\prod_{j\in
J}n_{j}{\boldsymbol{[}}\mathsf{fwdc}_{{q}}{\boldsymbol{]}}^{\nu_{n_{j}}}\mathrel{{}_{s_{2}}\\!\\!\sqsupseteq}\>M$

  * •

$\\{n_{j}:j\in J\\}\subseteq\nu_{m}\subseteq\\{n_{j}:j\in
J\\}\cup{\mathsf{nds}}(M)$

  * •

nodes in $\nu_{m}\cap{\mathsf{nds}}(M)$ cannot receive in the current round.

Let us apply the previous results to study how communication collisions
degrade the performances of gossip protocols. Let us reformulate the network
$\mathrm{GSP}_{2}$ of the previous section in a scenario with potential
communication collisions. Let us define

$\mathrm{{GSP}_{5}}\;\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}\;\;\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{s_{i}}}\>\;\big{|}\>\;\prod_{i=1}^{3}n_{i}{\boldsymbol{[}}\mathsf{fwdc}_{p}{\boldsymbol{]}}^{\nu_{n_{i}}}\>\;\big{|}\>\;d{\boldsymbol{[}}\mathsf{fwdc}_{1}{\boldsymbol{]}}^{\nu_{d}}$

with the same network topology as $\mathrm{GSP}_{2}$:
$\nu_{s_{1}}=\\{n_{1}\\}$, $\nu_{s_{2}}=\\{n_{1},n_{2}\\}$,
$\nu_{n_{1}}{=}\\{s_{1},s_{2},n_{3}\\}$, $\nu_{n_{2}}{=}\\{s_{2},n_{3}\\}$,
$\nu_{n_{3}}=\\{n_{1},n_{2},d\\}$ and $\nu_{d}=\\{n_{3},\mathit{tester}\\}$.
Note that, in the same round, the sender $s_{2}$ may broadcast to its
neighbours $n_{1}$ and $n_{2}$, whereas the sender $s_{1}$ may broadcast
(only) to its neighbour $n_{1}$, causing a failure at $n_{1}$.

As in the previous section, we will quantify the tolerance between the
gossiping network $\mathrm{GSP}_{5}$ and the network
$\mathrm{DONE}_{5}=\mathrm{DONE}_{2}$, in which at least one instance of the
message $v$ has been successfully propagated up to the destination node.

As a first step, we compute an estimation of the tolerance which allows
$\mathrm{GSP}_{5}$ to simulate $\mathrm{DONE}_{5}$, under the hypothesis that
the sender $s_{1}$ broadcasts to $n_{1}$ and the sender $s_{2}$ broadcasts to
$n_{1}$ and $n_{2}$, causing a failure at $n_{1}$. To this end, we derive the
following chain of similarities by applying, in sequence:  (i) Proposition
14(4) to nodes $n_{3}$ and $d$, together to Proposition 14(3) applied to node
$n_{2}$, to express that these nodes do not receive any message because there
are no transmitters in their neighbourhood, as a consequence, they are obliged
to timeout;  (ii) Theorem 19 in which node $n_{2}$ acts as a sender and
$n_{3}$ as a forwarder, together Proposition 14(2) to work underneath $\sigma$
prefixes;  (iii) Proposition 14(1) to remove a $\sigma$ prefix in $n_{2}$
together with Proposition 14(4) as node $d$ cannot receive message and hence
it timeouts;  (iv) Theorem 19 in which node $n_{3}$ acts as a sender and $d$
as a forwarder, together with Proposition 14(2) to work underneath $\sigma$
prefixes;  (v) Proposition 14(1) to remove $\sigma$ prefixes in $n_{3}$,
together with Proposition 14(3) as node $d$ is obliged to timeout. In all
steps, we reason up to parallel networks (Theorem 12).  For convenience, in
the chain below we define two auxiliary networks: $\mathrm{NET}_{h}$ and
$\mathrm{NET}_{i}$.

$\begin{array}[]{rrl}&&\mathrm{GSP}_{5}(s_{1}\mbox{ gossiped};s_{2}\mbox{
gossiped})\\\\[2.0pt]
&\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\;\big{|}\;n_{1}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{n_{1}}}\;\big{|}\;n_{2}{\boldsymbol{[}}\mathsf{resndc}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{n_{2}}}\;\big{|}\;n_{3}{\boldsymbol{[}}\mathsf{fwdc}_{p}{\boldsymbol{]}}^{\nu_{n_{3}}}\;\big{|}\;d{\boldsymbol{[}}\mathsf{fwdc}_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&\mathrel{{}_{0}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\;\big{|}\;n_{1}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{n_{1}}}\;\big{|}\;n_{2}{\boldsymbol{[}}\sigma.\mathsf{snd}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{n_{2}}}\;\big{|}\;n_{3}{\boldsymbol{[}}\sigma.\mathsf{fwdc}_{p}{\boldsymbol{]}}^{\nu_{n_{3}}}\;\big{|}\;d{\boldsymbol{[}}\sigma.\mathsf{fwdc}_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}&\mathrm{NET}_{h}\\\\[3.0pt]
&\mathrel{{}_{1-p}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\;\big{|}\;n_{1}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{n_{1}}}\;\big{|}\;n_{2}{\boldsymbol{[}}\sigma.\mathsf{nil}{\boldsymbol{]}}^{\nu_{n_{2}}}\;\big{|}\;n_{3}{\boldsymbol{[}}\sigma.{{\mathsf{resndc}\langle
v\rangle_{p}}}{\boldsymbol{]}}^{\nu_{n_{3}}}\;\big{|}\;d{\boldsymbol{[}}\sigma.\mathsf{fwdc}_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}&\mathrm{NET}_{i}\\\\[3.0pt]
&\mathrel{{}_{0}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\;\big{|}\;\prod^{2}_{i=1}n_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{n_{i}}}\;\big{|}\;n_{3}{\boldsymbol{[}}\sigma^{2}\mathsf{snd}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{n_{3}}}\;\big{|}\;d{\boldsymbol{[}}\sigma^{2}.\mathsf{fwdc}_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&\mathrel{{}_{1-p}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\;\big{|}\;\prod^{2}_{i=1}n_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{n_{i}}}\;\big{|}\;n_{3}{\boldsymbol{[}}\sigma^{2}.\mathsf{nil}{\boldsymbol{]}}^{\nu_{n_{3}}}\;\big{|}\;d{\boldsymbol{[}}\sigma^{2}.{{\mathsf{resndc}\langle
v\rangle_{1}}}{\boldsymbol{]}}^{\nu_{d}}\\\\[2.0pt]
&\mathrel{{}_{0}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\;\big{|}\;\prod^{3}_{i=1}n_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{n_{i}}}\;\big{|}\;d{\boldsymbol{[}}\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&=&\mathrm{DONE}_{5}.\end{array}$

Now, by transitivity (Proposition 7) we can derive the following equation:

$\mathrm{NET}_{i}\;\mathrel{{}_{1-p}\\!\\!\sqsupseteq}\;\mathrm{DONE}_{5}.$

Thus, we are in condition to apply Proposition 10, in which $M$, $N$, and $O$
are instantiated with $\mathrm{DONE}_{5}$, $\mathrm{NET}_{i}$, and
$\mathrm{NET}_{h}$, respectively, to derive the equation:

$\mathrm{NET}_{h}\;\mathrel{{}_{1-p^{2}}\\!\\!\sqsupseteq}\;\,\mathrm{DONE}_{5}$

where the tolerance $1-p^{2}$ is obtained by solving the expression
$(1-p)(1-(1-p))+(1-p)$. By transitivity on the first step of the chain above,
we can finally derive the equation:

$\mathrm{GSP}_{5}(s_{1}\mbox{ gossiped};s_{2}\mbox{
gossiped})\;\mathrel{{}_{1-p^{2}}\\!\\!\sqsupseteq}\;\,\mathrm{DONE}_{5}$ (7)

Similarly, we compute an estimation of the tolerance which allows
$\mathrm{GSP}_{5}$ to simulate $\mathrm{DONE}_{5}$, under the hypothesis that
the sender $s_{2}$ broadcasts to $n_{1}$ and $n_{2}$, and the sender $s_{1}$
does not transmit. To this end, we derive the following chain of similarities
by applying, in sequence:  (i) Proposition 14(3) to timeout nodes $n_{1}$ and
$n_{2}$, together with Proposition 14(4) to timeout nodes $n_{3}$ and $d$;
(ii) Theorem 19 in which $n_{1}$ and $n_{2}$ act as senders and $n_{3}$ as
forwarder, together with Proposition 14(2) to work underneath $\sigma$
prefixes;  (iii) Proposition 14(1) to remove $\sigma$ prefixes from $n_{1}$
and $n_{2}$, together with Proposition 14(3) to timeout $n_{3}$, together with
Proposition 14(4) to timeout $d$, together with Proposition 14(2) to work
underneath $\sigma$ prefixes;  (iv) Theorem 19 where $n_{3}$ acts as sender
and $d$ as forwarder, together with Proposition 14(2) to work underneath
$\sigma$ prefixes;  (v) Proposition 14(1) to remove $\sigma$ prefixes in
$n_{3}$, together with Proposition 14(3) to timeout node $d$.  As usual, in
all steps, we reason up to parallel composition (Theorem 12). For convenience,
in the chain below we define two auxiliary networks: $\mathrm{NET}_{l}$ and
$\mathrm{NET}_{m}$.

$\begin{array}[]{rrl}&&\mathrm{GSP}_{5}(s_{1}\mbox{ did not gossip}\mbox{;
}s_{2}\mbox{ gossiped})\\\\[2.0pt]
&\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\;\big{|}\;\prod^{2}_{i=1}n_{i}{\boldsymbol{[}}\mathsf{resndc}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{n_{i}}}\;\big{|}\;n_{3}{\boldsymbol{[}}\mathsf{fwdc}_{p}{\boldsymbol{]}}^{\nu_{n_{3}}}\;\big{|}\;d{\boldsymbol{[}}\mathsf{fwdc}_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&\mathrel{{}_{0}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\;\big{|}\;\prod^{2}_{i=1}n_{i}{\boldsymbol{[}}\sigma.\mathsf{snd}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{n_{i}}}\;\big{|}\;n_{3}{\boldsymbol{[}}\sigma.\mathsf{fwdc}_{p}{\boldsymbol{]}}^{\nu_{n_{3}}}\;\big{|}\;d{\boldsymbol{[}}\sigma.\mathsf{fwdc}_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}&\mathrm{NET}_{l}\\\\[3.0pt]
&\mathrel{{}_{1-q}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\;\big{|}\;\prod^{2}_{i=1}n_{i}{\boldsymbol{[}}\sigma.\mathsf{nil}{\boldsymbol{]}}^{\nu_{n_{i}}}\;\big{|}\;n_{3}{\boldsymbol{[}}\sigma.{\mathsf{resndc}\langle
v\rangle_{p}}{\boldsymbol{]}}^{\nu_{n_{3}}}\;\big{|}\;d{\boldsymbol{[}}\sigma.\mathsf{fwdc}_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}&\mathrm{NET}_{m}\\\\[3.0pt]
&\mathrel{{}_{0}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\;\big{|}\;\prod^{2}_{i=1}n_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{n_{i}}}\;\big{|}\;n_{3}{\boldsymbol{[}}\sigma^{2}.\mathsf{snd}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{n_{3}}}\;\big{|}\;d{\boldsymbol{[}}\sigma^{2}.\mathsf{fwdc}_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&\mathrel{{}_{1-p}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\;\big{|}\;\prod^{2}_{i=1}n_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{n_{i}}}\;\big{|}\;n_{3}{\boldsymbol{[}}\sigma^{2}.\mathsf{nil}{\boldsymbol{]}}^{\nu_{n_{3}}}\;\big{|}\;d{\boldsymbol{[}}\sigma^{2}.{{\mathsf{resndc}\langle
v\rangle_{1}}}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&\mathrel{{}_{0}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\;\big{|}\;\prod^{3}_{i=1}n_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{n_{i}}}\;\big{|}\;d{\boldsymbol{[}}\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&=&\mathrm{DONE}_{5}\end{array}$

with $q=2p(1{-}p)$. By transitivity (Proposition 7) we can derive the equation

$\mathrm{NET}_{m}\;\mathrel{{}_{1-p}\\!\\!\sqsupseteq}\;\,\mathrm{DONE}_{5}.$

Thus, we are in condition to apply Proposition 10, in which $M$, $N$, and $O$
are instantiated with $\mathrm{DONE}_{5}$, $\mathrm{NET}_{m}$, and
$\mathrm{NET}_{l}$, respectively, to derive the equation

$\mathrm{NET}_{l}\;\mathrel{{}_{1-2(p^{2}-p^{3})}\\!\\!\sqsupseteq}\;\,\mathrm{DONE}_{5}$

where the tolerance $1-2(p^{2}-p^{3})$ is obtained by solving the expression
$(1-p)(1-(1-q))+(1-q)$ with $q=2p(1{-}p)$. By transitivity on the first step
of the chain above, we can finally derive the equation

$\mathrm{GSP}_{5}(s_{1}\mbox{ did not gossip};s_{2}\mbox{
gossiped})\>\;\mathrel{{}_{1-2(p^{2}-p^{3})}\\!\\!\sqsupseteq}\>\;\,\mathrm{DONE}_{5}$
(8)

Now, let us denote with $\mathrm{GSP}_{5}(s_{1}[v]\mbox{; }s_{2}\mbox{
gossiped})$ the following network:

$s_{1}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{s_{1}}}\;\big{|}\;s_{2}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{2}}}\;\big{|}\;\prod^{2}_{i=1}n_{i}{\boldsymbol{[}}{\mathsf{resndc}\langle
v\rangle_{p}}{\boldsymbol{]}}^{\nu_{n_{i}}}\;\big{|}\;n_{3}{\boldsymbol{[}}\mathsf{fwdc}_{p}{\boldsymbol{]}}^{\nu_{n_{3}}}\;\big{|}\;d{\boldsymbol{[}}\mathsf{fwdc}_{1}{\boldsymbol{]}}^{\nu_{d}}.$

This is the gossip network $\mathrm{GSP}_{5}$ in which the sender $s_{2}$ has
already broadcast the message $v$ to its neighbours $n_{1}$ and $n_{2}$, and
the sender $s_{1}$ has still to decide whether to broadcast $v$ (to $n_{1}$)
or not. We can apply Corollary 20 to Equation 7 and Equation 8 to derive

$\mathrm{GSP}_{5}(s_{1}[v]\mbox{; }s_{2}\mbox{
gossiped})\;\mathrel{{}_{r}\\!\\!\sqsupseteq}\;\,\mathrm{DONE}_{5}$ (9)

with tolerance $r=1-2p^{2}+3p^{3}-2p^{4}$, obtained by solving
$p(1-p^{2})+(1-p)(1-2(p^{2}-p^{3}))$.

This gives us an estimation of the tolerance which allows the network
$\mathrm{GSP}_{5}$ to simulate the network $\mathrm{DONE}_{5}$ when the sender
$s_{2}$ has already broadcast the message $v$ to its neighbours $n_{1}$ and
$n_{2}$, whereas the sender $s_{1}$ has still to decide whether to broadcast
$v$ (to $n_{1}$) or not.

Similarly, we compute an estimation of the tolerance which allows the network
$\mathrm{GSP}_{5}$ to simulate the network $\mathrm{DONE}_{5}$ when the sender
$s_{2}$ has decided not to broadcast the message $v$, while $s_{1}$ has still
to decide whether to broadcast $v$ or not. To this end, we derive the
following chain of similarities by applying, in sequence:  (i) Theorem 19
where $s_{1}$ broadcasts its message and $n_{1}$ receives it;  (ii)
Proposition 14(3) to timeout node $n_{1}$, together with Proposition 14(4) to
timeout nodes $n_{2}$, $n_{3}$, and $d$;  (iii) Theorem 19 where $n_{1}$ acts
as transmitter and $n_{3}$ as receiver, together with Proposition 14(2) to
work underneath $\sigma$ prefixes;  (iv) Proposition 14(1) to remove the
$\sigma$ prefix in $n_{1}$, together with Proposition 14(4) to timeout nodes
$n_{2}$ and $d$, and Proposition 14(3) to timeout $n_{3}$;  (v) Theorem 19 in
which $n_{3}$ transmits its value and both $n_{2}$ and $d$ receive it,
together with Proposition 14(2) to work underneath $\sigma$ prefixes;  (vi)
Proposition 14(1) to remove $\sigma$ prefixes from $n_{3}$, together with
Proposition 14(3) to timeout $n_{2}$; Proposition 14(5) to model that the
transmission of $n$ gets lost, together with Proposition 14(2) to work
underneath $\sigma$ prefixes.  As done before, in all steps we use Theorem 12
to reason up to parallel components. For convenience, in the chain below we
define three auxiliary networks: $\mathrm{NET}_{n}$, $\mathrm{NET}_{o}$ and
$\mathrm{NET}_{t}$.

$\begin{array}[]{rrl}&&\mathrm{GSP}_{5}(s_{1}[v]\mbox{; }s_{2}\mbox{ did not
gossip})\\\\[2.0pt]
&\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}&s_{1}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{s_{1}}}\;\big{|}\;s_{2}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{2}}}\;\big{|}\;\prod_{i=1}^{3}n_{i}{\boldsymbol{[}}\mathsf{fwdc}_{p}{\boldsymbol{]}}^{\nu_{n_{i}}}\;\big{|}\;d{\boldsymbol{[}}\mathsf{fwdc}_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&\mathrel{{}_{1-p}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\;\big{|}\;n_{1}{\boldsymbol{[}}\mathsf{resndc}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{n_{1}}}\;\big{|}\;\prod^{3}_{j=2}n_{j}{\boldsymbol{[}}\mathsf{fwdc}_{p}{\boldsymbol{]}}^{\nu_{n_{j}}}\;\big{|}\;d{\boldsymbol{[}}\mathsf{fwdc}_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}&\mathrm{NET}_{n}\\\\[3.0pt]
&\mathrel{{}_{0}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\;\big{|}\;n_{1}{\boldsymbol{[}}\sigma.\mathsf{snd}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{n_{1}}}\;\big{|}\;\prod^{3}_{i=2}n_{i}{\boldsymbol{[}}\sigma.\mathsf{fwdc}_{p}{\boldsymbol{]}}^{\nu_{n_{i}}}\;\big{|}\;d{\boldsymbol{[}}\sigma.\mathsf{fwdc}_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}&\mathrm{NET}_{o}\\\\[3.0pt]
&\mathrel{{}_{1-p}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\;\big{|}\;n_{1}{\boldsymbol{[}}\sigma.\mathsf{nil}{\boldsymbol{]}}^{\nu_{n_{1}}}\;\big{|}\;n_{2}{\boldsymbol{[}}\sigma.\mathsf{fwdc}_{p}{\boldsymbol{]}}^{\nu_{n_{2}}}\;\big{|}\;n_{3}{\boldsymbol{[}}\sigma.\mathsf{resndc}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{n_{3}}}\;\big{|}\;d{\boldsymbol{[}}\sigma.\mathsf{fwdc}_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}&\mathrm{NET}_{t}\\\\[3.0pt]
&\mathrel{{}_{0}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\;\big{|}\;n_{1}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{n_{1}}}\;\big{|}\;n_{2}{\boldsymbol{[}}\sigma^{2}.\mathsf{fwdc}_{p}{\boldsymbol{]}}^{\nu_{n_{2}}}\;\big{|}\;n_{3}{\boldsymbol{[}}\sigma^{2}.\mathsf{snd}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{n_{3}}}\;\big{|}\;d{\boldsymbol{[}}\sigma^{2}.\mathsf{fwdc}_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&\mathrel{{}_{1-p}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\;\big{|}\;n_{1}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{n_{1}}}\;\big{|}\;n_{2}{\boldsymbol{[}}\sigma^{2}.\mathsf{resndc}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{n_{2}}}\;\big{|}\;n_{3}{\boldsymbol{[}}\sigma^{2}.\mathsf{nil}{\boldsymbol{]}}^{\nu_{n_{3}}}\;\big{|}\;d{\boldsymbol{[}}\sigma^{2}.\mathsf{resndc}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&\mathrel{{}_{0}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\;\big{|}\;n_{1}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{n_{1}}}\;\big{|}\;n_{2}{\boldsymbol{[}}\sigma^{3}.\mathsf{snd}\langle
v\rangle_{p}{\boldsymbol{]}}^{\nu_{n_{2}}}\;\big{|}\;n_{3}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{n_{3}}}\;\big{|}\;d{\boldsymbol{[}}\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&\mathrel{{}_{0}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\;\big{|}\;\prod^{3}_{i=1}n_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{n_{i}}}\;\big{|}\;d{\boldsymbol{[}}\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&=&\mathrm{DONE}_{5}\,.\end{array}$

By transitivity (Proposition 7) we can derive the equation

$\mathrm{NET}_{t}\;\mathrel{{}_{1-p}\\!\\!\sqsupseteq}\;\,\mathrm{DONE}_{5}.$

This allows us to apply Proposition 10, in which $M$, $N$, and $O$ are
instantiated with $\mathrm{DONE}_{5}$, $\mathrm{NET}_{t}$, and
$\mathrm{NET}_{o}$, respectively, to derive the equation

$\mathrm{NET}_{o}\;\mathrel{{}_{1-p^{2}}\\!\\!\sqsupseteq}\;\,\mathrm{DONE}_{5}$

where the tolerance $1-p^{2}$ is obtained by solving the expression
$(1-p)(1-(1-p))+(1-p)$. Then, by transitivity (Proposition 7) we can easily
derive

$\mathrm{NET}_{n}\;\mathrel{{}_{1-p^{2}}\\!\\!\sqsupseteq}\;\,\mathrm{DONE}_{5}.$

This last equation can be used to apply Proposition 9, in which $M$, $N$, and
$O$ are instantiated with $\mathrm{DONE}_{5}$, $\mathrm{NET}_{n}$, and
$\mathrm{GSP}_{5}(s_{1}[v]\mbox{; }s_{2}\mbox{ did not gossip})$,
respectively, to derive:

$\begin{array}[]{c}\mathrm{GSP}_{5}(s_{1}[v]\mbox{; }s_{2}\mbox{ did not
gossip})\mathrel{{}_{1-p^{3}}\\!\\!\sqsupseteq}\>\;\,\mathrm{DONE}_{5}\end{array}$
(10)

where the tolerance $1-p^{3}$ is obtained by solving the expression
$(1-p)(1-(1-p^{2}))+(1-p^{2})$.

Now, by applying Corollary 21 to Equation 9 and Equation 10 we can combine the
two probabilistic behaviours of the sender $s_{2}$, thus obtaining:

$\mathrm{GSP}_{5}\;\mathrel{{}_{r}\\!\\!\sqsupseteq}\;\,\mathrm{DONE}_{5}$

with tolerance $r=1-(3p^{3}-4p^{4}+2p^{5})$ obtained by solving
$p(1-2p^{2}+3p^{3}-2p^{4})+(1-p)(1-p^{3})$. This says that the gossip network
$\mathrm{GSP}_{5}$ will succeed in transmitting the message $v$ to the
destination $d$ with probability (at least) $3p^{3}-4p^{4}+2p^{5}$.

In the previous section, we have seen that in the absence of collisions, the
success probability of $\mathrm{GSP}_{2}$ is (at least) $3p^{3}-2p^{4}$. Since
$3p^{3}-4p^{4}+2p^{5}<3p^{3}-2p^{4}$, for any $p>0$, it follows that the
presence of collisions downgrades the performance of this small network of
$2p^{4}-2p^{5}$. Thus, for instance, for a gossip probability $p=0.8$ the
destination node in $\mathrm{GSP}_{5}$ will receive the message with
probability (at least) $0.55$, whereas in $\mathrm{GSP}_{2}$ this probability
is $0.716$; similarly for $p=0.9$ the probability of success in
$\mathrm{GSP}_{5}$ is about $0.74$ while in $\mathrm{GSP}_{2}$ it is $0.88$.
In bigger networks, with more collisions, the degradation will be much more
evident.

######  Remark 22.

Due to its general formulation, Theorem 18, dealing with message propagation
in paths of different lengths, is valid also in the presence of communication
collisions.

##  5\. Random delays to mitigate the effects of collisions

In this section, we show how pTCWS can be used to model and reason on
_randomised gossip protocols_ , where messages may be broadcast in different
time instants, according to some probability distribution (see, _e.g._ ,
[FG06]). In this manner, if there is a potential collision at a given round
there are still chances that the message will reach the final destination in
the following rounds, improving the probability of success of the gossip
protocol.

Randomisation may be implemented in different ways. For instance, one may
decide to broadcast messages according to a _uniform probability distribution_
within a _discrete_ time interval $1{..}k$, for $k\in\mathbb{N}$. This means
that the message may be transmitted in each of the $k$ time instants, with a
probability $\frac{1}{k}$. In such a scenario, both sender and forwarder
processes should be reformulated as follows:

$\begin{array}[]{rcl}{\mathsf{sndu}\langle
v\rangle}_{p_{\mathrm{g}},k}&\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}&\tau.\big{(}\tau.(\bigoplus_{i=1}^{k}\frac{1}{k}{\colon}\sigma^{i}.\mathsf{snd}\langle
v\rangle_{1})\oplus_{p_{\mathrm{g}}}\mathsf{nil}\big{)}\\\\[1.0pt]
\mathsf{resndu}\langle
v\rangle_{p_{\mathrm{g}},k}&\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}&\lfloor?(y){\mathsf{nil}}\rfloor{\mathsf{sndu}\langle
v\rangle}_{p_{\mathrm{g}},k}\\\\[1.0pt]
\mathsf{fwdu}_{p_{\mathrm{g}},k}&\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}&{?(x).\mathsf{resndu}\langle
x\rangle_{p_{\mathrm{g}},k}}.\end{array}$

The main algebraic instrument to reason on the performance of the protocol
remains message propagation. The following result is a straightforward
reformulation of Theorem 19. In Corollary 23, for simplicity, we have only one
sender that broadcasts with probability $1$. This sender derives by the
resolution of the probabilistic choice within any term ${\mathsf{sndu}\langle
v\rangle}_{p_{\mathrm{g}},k}$.

######  Corollary 23 (Message propagation with collisions and random delays).

Let $J$ be a subset of $\mathbb{N}$. Let $M$ be a well-formed network defined
by

$M\equiv N\>\;\big{|}\>\;m{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{m}}\>\;\big{|}\>\;\prod_{j\in
J}n_{j}{\boldsymbol{[}}\mathsf{fwdu}_{q_{j},k}{\boldsymbol{]}}^{\nu_{n_{j}}}$

such that:  (1) $\\{n_{j}\mid j\in
J\\}\subseteq\nu_{m}\subseteq{\mathsf{nds}}(M)$, and  (2) the nodes in
$\nu_{m}\cap{\mathsf{nds}}(N)$ cannot receive in the current round.  Then,

$M\;\mathrel{{}_{0}\\!\\!\sqsupseteq}\;N\;|\;m{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m}}\;|\;\prod_{j\in
J}n_{j}{\boldsymbol{[}}\mathsf{resndu}\langle
v\rangle_{q_{j},k}{\boldsymbol{]}}^{\nu_{n_{j}}}.$

In the rest of this section, we will apply Corollary 23 to reason on a variant
of the network $\mathrm{GSP}_{1}$ of Section 3 where random delays are
introduced.

Consider a gossiping network $\mathrm{GSP}_{6}$, with gossip probability $p$,
composed by two source nodes $s_{1}$ and $s_{2}$ that may delay their
transmission within a discrete time interval $1{..}2$, and a destination node
$d$. The network is the following:

$\mathrm{GSP}_{6}\>\;\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}\;\>\;\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{sndu}\langle
v\rangle_{p,2}{\boldsymbol{]}}^{\nu_{s_{i}}}\>\;\big{|}\>\;d{\boldsymbol{[}}\mathsf{fwdu}_{1,1}{\boldsymbol{]}}^{\nu_{d}}$

where $\nu_{s_{1}}=\nu_{s_{2}}=\\{d\\}$ and
$\nu_{d}{=}\\{s_{1},s_{2},\mathit{tester}\\}$.

Our goal is to estimate the distance between $\mathrm{GSP}_{6}$ and a network
$\mathrm{DONE}_{6}$ in which the message $v$ propagated up to the destination
node $d$ that will rebroadcast the message according to some probabilistic
delay depending on the probability $p$.

$\mathrm{DONE}_{6}\;\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}\;\;\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\>\;\big{|}\>\;d{\boldsymbol{[}}\tau.(\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}\,\oplus_{(\frac{1}{2}{+}\frac{p^{2}}{2})}\,\sigma^{4}.\mathsf{snd}\langle
v\rangle_{1}){\boldsymbol{]}}^{\nu_{d}}.$

At the end of this section, we will show that
$\mathrm{GSP}_{6}\mathrel{{}_{r}\\!\\!\sqsupseteq}\mathrm{DONE}_{6}$, with
tolerance $r=1-(2p-\frac{3}{2}p^{2})$. In order to estimate the tolerance $r$
we distinguish three possible cases, depending whether the sender nodes
$s_{1}$ and $s_{2}$ eventually transmit or not. More precisely, we estimate
the tolerance of the simulation in the following cases:  (a) node $s_{1}$
transmits while $s_{2}$ does not,  (b) node $s_{2}$ transmits while $s_{1}$
does not,  (c) both nodes $s_{1}$ and $s_{2}$ transmit.  Notice that we do not
analyse the case when neither $s_{1}$ nor $s_{2}$ transmits, since such a
behaviour does not allow $\mathrm{GSP}_{6}$ to simulate $\mathrm{DONE}_{6}$.
Then, by applying Theorem 18 to compose different paths we combine the
tolerances obtained in cases (b) and (c) to get the tolerance when $s_{2}$
transmits independently whether $s_{1}$ transmits or not. Finally, we use
again Theorem 18 to combine this tolerance with that obtained from case (a) to
infer $r$.

Let us analyse these three different cases.

#### (a) Node $s_{1}$ transmits while $s_{2}$ does not.

In this case, there are obviously no collisions and the message will
eventually reach the destination. Now, if $s_{1}$ decides to transmit with a
delay of $h$ time units, for $h\in\\{1,2\\}$, then, by applying in sequence:
(i) Proposition 14(4) to timeout node $d$, as for $h$ rounds it will not get
any message;  (ii) Corollary 23 to propagate the message from the sender
$s_{1}$ to the node $d$, together with Proposition 14(2) to work underneath
$\sigma$ prefixes;  (iii) Proposition 14(1) to remove $\sigma$ prefixes in
$s_{1}$;  (iv) Proposition 14(3) together with the straightforward equation
$d{\boldsymbol{[}}{\mathsf{sndu}\langle
v\rangle}_{1,1}{\boldsymbol{]}}^{\nu_{d}}\mathrel{{}_{0}\\!\\!\sqsupseteq}d{\boldsymbol{[}}{\sigma.{\mathsf{snd}\langle
v\rangle}_{1}}{\boldsymbol{]}}^{\nu_{d}}$;  it follows that:

$\begin{array}[]{rrl}&&\mathrm{GSP}_{6}(s_{1}\mbox{ sends in }h\mbox{ rounds;
}s_{2}\mbox{ did not gossip})\\\\[2.0pt]
&\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}&s_{1}{\boldsymbol{[}}\sigma^{h}.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{s_{1}}}\;\big{|}\;s_{2}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{2}}}\;\big{|}\;d{\boldsymbol{[}}\mathsf{fwdu}_{1,1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&\mathrel{{}_{0}\\!\\!\sqsupseteq}&s_{1}{\boldsymbol{[}}\sigma^{h}.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{s_{1}}}\;\big{|}\;s_{2}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{2}}}\;\big{|}\;d{\boldsymbol{[}}\sigma^{h}.\mathsf{fwdu}_{1,1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&\mathrel{{}_{0}\\!\\!\sqsupseteq}&s_{1}{\boldsymbol{[}}\sigma^{h}.\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{1}}}\;\big{|}\;s_{2}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{2}}}\;\big{|}\;d{\boldsymbol{[}}\sigma^{h}.\mathsf{resndu}\langle
v\rangle_{1,1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&\mathrel{{}_{0}\\!\\!\sqsupseteq}&s_{1}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{1}}}\;\big{|}\;s_{2}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{2}}}\;\big{|}\;d{\boldsymbol{[}}\sigma^{h}.\mathsf{resndu}\langle
v\rangle_{1,1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&\mathrel{{}_{0}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\;\big{|}\;d{\boldsymbol{[}}\sigma^{h+2}.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{d}}.\end{array}$

By transitivity (Proposition 7) we can derive:

$\mathrm{GSP}_{6}(s_{1}\mbox{ sends in }h\mbox{ rounds; }s_{2}\mbox{ did not
gossip})\;\mathrel{{}_{0}\\!\\!\sqsupseteq}\;\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\>\;\big{|}\>\;d{\boldsymbol{[}}\sigma^{h+2}.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{d}}$ (11)

We know that $s_{1}$ transmits in $\mathrm{GSP}_{6}$ according to a uniform
distribution probability in the time interval $1{..}2$. Thus, by an
application of Theorem 18, we can combine the two instances of Equation 11,
for $h=1$ and $h=2$, to obtain:

$\begin{array}[]{rl}&\mathrm{GSP}_{6}(s_{1}\mbox{ sends in $1$ or $2$ rounds;
}s_{2}\mbox{ did not gossip})\\\\[2.0pt]
\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}&s_{1}{\boldsymbol{[}}\tau.(\sigma.\mathsf{snd}\langle
v\rangle_{1}\oplus_{\frac{1}{2}}\sigma^{2}.\mathsf{snd}\langle
v\rangle_{1}){\boldsymbol{]}}^{\nu_{s_{1}}}\;\big{|}\;s_{2}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{2}}}\;\big{|}\;d{\boldsymbol{[}}\mathsf{fwdu}_{1,1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
\mathrel{{}_{0}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\;\big{|}\;d{\boldsymbol{[}}\tau.(\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}\oplus_{\frac{1}{2}}\sigma^{4}.\mathsf{snd}\langle
v\rangle_{1}){\boldsymbol{]}}^{\nu_{d}}.\end{array}$ (12)

The complete behaviour of $s_{1}$ can be derived by the following chain of
similarities, obtained by an application of Proposition 11(1) and Equation 12:

$\begin{array}[]{rrl}&&\mathrm{GSP}_{6}(s_{1}[v]\mbox{; }s_{2}\mbox{ did not
gossip})\\\\[2.0pt]
&\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}&s_{1}{\boldsymbol{[}}\mathsf{sndu}\langle
v\rangle_{p,2}{\boldsymbol{]}}^{\nu_{s_{1}}}\;\big{|}\;s_{2}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{2}}}\;\big{|}\;d{\boldsymbol{[}}\mathsf{fwdu}_{1,1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
&\mathrel{{}_{1-p}\\!\\!\sqsupseteq}&s_{1}{\boldsymbol{[}}\tau.(\sigma.\mathsf{snd}\langle
v\rangle_{1}\oplus_{\frac{1}{2}}\sigma^{2}.\mathsf{snd}\langle
v\rangle_{1}){\boldsymbol{]}}^{\nu_{s_{1}}}\;\big{|}\;s_{2}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{2}}}\;\big{|}\;d{\boldsymbol{[}}\mathsf{fwdu}_{1,1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]