17123 LABEL:LastPageDec. 17, 2019Mar. 18, 2021

# Reconfiguration and message losses
in parameterized broadcast networks

Nathalie Bertranda  ,  Patricia Bouyerb  and  Anirban Majumdara,b  aUniv.
Rennes, Inria, CNRS, IRISA — Rennes (France)  bLSV, CNRS & ENS Paris-Saclay,
Univ. Paris-Saclay — Cachan (France)

###### Abstract.

Broadcast networks allow one to model networks of identical nodes
communicating through message broadcasts. Their parameterized verification
aims at proving a property holds for any number of nodes, under any
communication topology, and on all possible executions. We focus on the
coverability problem which dually asks whether there exists an execution that
visits a configuration exhibiting some given state of the broadcast protocol.
Coverability is known to be undecidable for static networks, _i.e._ when the
number of nodes and communication topology is fixed along executions. In
contrast, it is decidable in PTIME when the communication topology may change
arbitrarily along executions, that is for reconfigurable networks.
Surprisingly, no lower nor upper bounds on the minimal number of nodes, or the
minimal length of covering execution in reconfigurable networks, appear in the
literature.

In this paper we show tight bounds for cutoff and length, which happen to be
linear and quadratic, respectively, in the number of states of the protocol.
We also introduce an intermediary model with static communication topology and
non-deterministic message losses upon sending. We show that the same tight
bounds apply to lossy networks, although, reconfigurable executions may be
linearly more succinct than lossy executions. Finally, we show NP-completeness
for the natural optimisation problem associated with the cutoff.

##  1\. Introduction

#### Parameterized verification.

Systems formed of many identical agents arise in many concrete areas:
distributed algorithms, populations, communication or cache-coherence
protocols, chemical reactions etc. Models for such systems depend on the
communication or interaction means between the agents. For example pairwise
interactions are commonly used for populations of individuals, whereas
selective broadcast communications are more relevant for communication
protocols on ad-hoc networks. The capacity of the agents, and thus models that
are used to represent their behaviour also vary.

Verifying such systems amounts to checking that a property holds independently
of the number of agents. Typically, a consensus algorithm should be correct
for any number of participants. We refer to these systems as parameterized
systems, and the parameter is the number of agents. The verification of
parameterized systems started in the late 1980’s and recently regained
attention from the model-checking community [Suz88, GS92, Esp14, BJK+15]. It
can be seen as particular cases of infinite-state-system verification, and the
fact that all agents are identical can sometimes lead to efficient algorithms
[ES96].

#### Broadcast networks.

This paper targets the application to protocols over ad-hoc networks, and we
thus focus on the model of broadcast networks [DSZ10]. A broadcast network is
composed of several nodes that execute the same broadcast protocol. The latter
is a finite automaton, where transitions are labeled with message sendings or
message receptions. Configuration in broadcast networks is then comprised of a
set of agents, their current local states, together with a communication
topology (which represents which agents are within radio range). A transition
represents the effect of one agent sending a message to its neighbours.

Parameterized verification of broadcast networks amounts to checking a given
property independently of the initial configuration, and in particular
independently of the number of agents and communication topology. A natural
property one can be interested in is coverability: whether there exists an
execution leading to a configuration in which one node is in a given local
state. When considering error states, a positive instance for the coverability
problem thus corresponds to a network that can exhibit a bad behaviour.

Coverability is undecidable for static broadcast networks [DSZ10], _i.e._ when
the communication topology is fixed along executions. Decidability can be
recovered by relaxing the semantics and allowing non-deterministic
reconfigurations of the communication topology. In reconfigurable broadcast
networks, coverability of a control state is decidable in PTIME [DSTZ12]. A
simple saturation algorithm allows to compute the set of all states of the
broadcast protocol that can be covered.

#### Cutoff and covering length.

Two important characteristics of positive instances of the coverability
problem are the cutoff and the covering length. First, the _cutoff_ is the
minimal number of agents for which a covering execution exists. The notion of
cutoff is particularly relevant for reconfigurable broadcast networks since
they enjoy a monotonicity property: if a state can be covered from a
configuration, it can also be from any configuration with more nodes. Second,
the _covering length_ is the minimal number of steps for covering executions.
It weighs how fast a network execution can go wrong. Both the cutoff and the
covering length are somehow complexity measures for the coverability problem.
Surprisingly, no upper nor lower bounds on these values appear in the
literature for reconfigurable broadcast networks.

#### Contributions.

In this paper, we prove a tight linear bound for the cutoff, and a tight
quadratic bound for the covering length in reconfigurable broadcast networks.
Both are expressed in the number of states of the broadcast protocol. These
are obtained by refining the saturation algorithm that computes the set of
coverable states, and finely analysing it.

Another contribution is to introduce lossy broadcast networks, in which the
communication topology is fixed, however errors in message transmission may
occur. In contrast with broadcast networks with losses that appear in the
literature [DSZ12], in our model, message losses happen upon sending, rather
than upon reception. This makes a crucial difference: reconfiguration of the
communication topology can easily be encoded by losses upon reception, whereas
it is not obvious for losses upon sending. Perhaps surprisingly, we prove that
the set of states that can be covered in reconfigurable semantics agrees with
the one in static lossy semantics. Using the same refined saturation
algorithm, we prove that same tight bounds hold for lossy broadcast networks:
the cutoff is linear, and the covering length is quadratic (in the number of
states of the broadcast protocol). The two semantics thus appear quite
similar, yet, we show that the reconfigurable semantics can be linearly more
succinct (in terms of number of nodes) than the lossy semantics.

Finally, we study a natural decision problem related to the cutoff: decide
whether a state is coverable (in either semantics) with a fixed number of
nodes. We prove it to be NP-complete.

#### Outline.

In Section 2, we define the broadcast networks, with static, reconfiurable and
lossy semantics. In Section 3, we present our tight bounds for cutoff and
covering length. In Section 4, we show our succinctness result. In Section 5,
we give our NP-completeness result.

##  2\. Broadcast networks

###  2.1. Static broadcast networks

A _broadcast protocol_ is a tuple $\mathcal{P}=(Q,I,\Sigma,\Delta)$ where $Q$
is a finite set of control states; $I\subseteq Q$ is the set of initial
control states; $\Sigma$ is a finite alphabet; and
$\Delta\subseteq(Q\times\\{!\textit{a},?\textit{a}\mid a\in\Sigma\\}\times Q)$
is the transition relation.

For ease of readability, we often write $q\xrightarrow{!\textit{a}}q^{\prime}$
(resp. $q\xrightarrow{?\textit{a}}q^{\prime}$) for
$(q,!\textit{a},q^{\prime})\in\Delta$ (resp.
$(q,?\textit{a},q^{\prime})\in\Delta$). We assume all broadcast networks to be
complete for receptions: for every $q\in Q$ and $a\in\Sigma$, there exists
$q^{\prime}$ such that $q\xrightarrow{?\textit{a}}q^{\prime}$.

A broadcast protocol is represented in Figure 1. In this example and in the
whole paper, for concision purposes, we assume that if the reception of a
message is unspecified from some state, it implicitly represents a self-loop.
For example here, from $q_{1}$, receiving $a$ leads to $q_{1}$ again.

$\scriptstyle q_{0}$$\scriptstyle q_{1}$$\scriptstyle q_{2}$$\scriptstyle
q_{3}$$\scriptstyle q_{4}$$\scriptstyle
r_{1}$$\scriptstyle\bot$$\scriptstyle\Smiley[2]$$\scriptstyle!\textit{a}$$\scriptstyle?\textit{a}$$\scriptstyle!\textit{b}_{1}$$\scriptstyle?\textit{a}$$\scriptstyle!\textit{b}_{2}$$\scriptstyle?\textit{b}_{1}$$\scriptstyle?\textit{b}_{2}$$\scriptstyle?\textit{b}_{i}$
Figure 1. Example of a broadcast protocol.

Broadcast networks involve several copies, or _nodes_ , of the same broadcast
protocol $\mathcal{P}$. A configuration is an undirected graph whose vertices
are labelled with a state of $Q$. Transitions between configurations happen by
broadcasts from a node to its neighbours.

Formally, given a broadcast protocol $\mathcal{P}=(Q,I,\Sigma,\Delta)$, a
_configuration_ is an undirected graph
$\gamma=(\mathsf{N},\mathsf{E},\mathsf{L})$ where $\mathsf{N}$ is a finite set
of nodes; $\mathsf{E}\subseteq\mathsf{N}\times\mathsf{N}$ is a symmetric and
irreflexive relation describing the set of edges; finally,
$\mathsf{L}\colon\mathsf{N}\to Q$ is the labelling function. We let
$\Gamma(\mathcal{P})$ denote the (infinite) set of $Q$-labelled graphs. Given
a configuration $\gamma\in\Gamma(\mathcal{P})$, we write
$\mathsf{n}\sim\mathsf{n}^{\prime}$ whenever
$(\mathsf{n},\mathsf{n}^{\prime})\in\mathsf{E}$ and we let
$\mathsf{Neigh}_{\gamma}(\mathsf{n})=\\{\mathsf{n}^{\prime}\in\mathsf{N}\mid\mathsf{n}\sim\mathsf{n}^{\prime}\\}$
be the neighbourhood of $\mathsf{n}$, _i.e._ the set of nodes adjacent to
$\mathsf{n}$. Finally $\mathsf{L}(\gamma)$ denotes the set of labels appearing
in nodes of $\gamma$. A configuration $(\mathsf{N},\mathsf{E},\mathsf{L})$ is
called _initial_ if $\mathsf{L}(\mathsf{N})\subseteq I$.

The operational semantics of a static broadcast network for a given broadcast
protocol $\mathcal{P}$ is an infinite-state transition system
$\mathcal{T}(\mathcal{P})$. Intuitively, each node of a configuration runs
protocol $\mathcal{P}$, and may send/receive messages to/from its neighbours.
From a configuration $\gamma=(\mathsf{N},\mathsf{E},\mathsf{L})$, there is a
step to
$\gamma^{\prime}=(\mathsf{N}^{\prime},\mathsf{E}^{\prime},\mathsf{L}^{\prime})$
if $\mathsf{N}^{\prime}=\mathsf{N}$, $\mathsf{E}^{\prime}=\mathsf{E}$, and
there exists $\mathsf{n}\in\mathsf{N}$ and $a\in\Sigma$ such that
$(\mathsf{L}(\mathsf{n}),!\textit{a},\mathsf{L}^{\prime}(\mathsf{n}))\in\Delta$,
and for every $\mathsf{n}^{\prime}\in\mathsf{N}$, if
$\mathsf{n}^{\prime}\in\mathsf{Neigh}_{\gamma}(\mathsf{n})$, then
$(\mathsf{L}(\mathsf{n}^{\prime}),?\textit{a},\mathsf{L}^{\prime}(\mathsf{n}^{\prime}))\in\Delta$,
otherwise
$\mathsf{L}^{\prime}(\mathsf{n}^{\prime})=\mathsf{L}(\mathsf{n}^{\prime})$: a
step reflects how nodes evolve when one of them broadcasts a message to its
neighbours. We write
$\gamma\xrightarrow{\mathsf{n},!\textit{a}}_{\mathtt{s}}\gamma^{\prime}$, or
simply $\gamma\to_{\mathtt{s}}\gamma^{\prime}$ (the $\mathtt{s}$ subscript
emphasizes that the communication topology is _static_).

An _execution_ of the static broadcast network is a sequence
$\rho={(\gamma_{i})}_{0\leq i\leq r}$ of configurations
$(\mathsf{N},\mathsf{E},\mathsf{L}_{i})$ such that $\gamma_{0}$ is an initial
configuration, and for every $0\leq i<r$,
$\gamma_{i}\to_{\mathtt{s}}\gamma_{i+1}$. We write $\textsf{\\#nodes}(\rho)$
for the number of nodes in $\gamma_{0}$, $\textsf{\\#steps}(\rho)$ for the
number $r$ of steps along $\rho$, and for any node
$\mathsf{n}\in\mathsf{N},\textsf{\\#steps}(\rho,\mathsf{n})$ for the number of
broadcasts, called the _active length_ , of node $\mathsf{n}$ along $\rho$.
Note that, along an execution, the number of nodes and the communication
topology are fixed. The set of all static executions is denoted
$\mathsf{Exec}_{\mathtt{s}}(\mathcal{P})$.

We provide an example of a static execution in Figure 2 for the broadcast
protocol of Figure 1. Note that the communication topology is the same
throughout the execution. In the example, the colored nodes broadcast a
message to its neighbours in the step leading to the next configuration.

$q_{0}$$q_{0}$$q_{0}$$q_{0}$$q_{0}$$\xrightarrow{!\textit{a}}_{\mathtt{s}}$$q_{1}$$q_{0}$$q_{0}$$q_{1}$$q_{0}$$\xrightarrow{!\textit{b}_{1}}_{\mathtt{s}}$$q_{2}$$r_{1}$$\bot$$q_{1}$$q_{0}$$\xrightarrow{!\textit{b}_{1}}_{\mathtt{s}}$$q_{2}$$r_{1}$$\bot$$q_{2}$$\bot$

Figure 2. A sample static execution for the protocol from Figure 1.

####  Coverability problem.

Given a broadcast protocol $\mathcal{P}$ and a subset of target states
$F\subseteq Q$, we write $\mathsf{COVER}_{\mathtt{s}}(\mathcal{P},F)$ for the
set of all _covering_ executions, that is, executions that visit a
configuration with a node labelled by a state in $F$:

$\mathsf{COVER}_{\mathtt{s}}(\mathcal{P},F)=\\{{(\gamma_{i})}_{0\leq i\leq
r}\in\mathsf{Exec}_{\mathtt{s}}(\mathcal{P})\mid\mathsf{L}(\gamma_{r})\cap
F\not=\emptyset\\}.\enspace$

The _coverability problem_ is a decision problem that takes a broadcast
protocol $\mathcal{P}$ and a subset of target states $F$ as inputs, and
outputs whether $\mathsf{COVER}_{\mathtt{s}}(\mathcal{P},F)$ is nonempty. For
broadcast networks, the coverability problem is a parameterized verification
problem, since the number of initial configurations is infinite. It is known
that coverability is undecidable for static broadcast networks [DSZ10], since
one can use the communication topology to build chains that may encode values
of counters, and hence simulate Minsky machines [Min67].

Back to the example in Figure 1, one can show that from any initial
configuration, the target state $\Smiley$ cannot be covered under the static
semantics: $\mathsf{COVER}_{\mathtt{s}}(\mathcal{P},\Smiley)=\emptyset$.
Indeed, in order to cover $\Smiley$, one node –say $\mathsf{n}$– must reach
$q_{4}$ by performing the broadcasts of $b_{1}$ and $b_{2}$. Node $\mathsf{n}$
must be linked to at least one other node $\mathsf{n}^{\prime}$ that performs
the second broadcast of $a$ and make $\mathsf{n}$ move from $q_{2}$ to
$q_{3}$. However, because of the static topology after $\mathsf{n}$ had
broadcast $b_{1}$, $\mathsf{n}^{\prime}$ could no longer be in $q_{0}$, and
thus would not have been able to broadcast $a$.

If the broadcast protocol $\mathcal{P}$ allows to cover the subset $F$, we
define the _cutoff_ as the minimal number of nodes required in an execution to
cover $F$. Similarly, we define the _covering length_ as the length of a
shortest finite execution covering $F$. Those values are important to
characterize the complexity of a broadcast protocol: assuming a safe set of
states, coverability of the complement set represents bad behaviours, and
cutoff and covering length measure the size of minimal witnesses for violation
of the safety property.

###  2.2. Reconfigurable broadcast networks

To circumvent the undecidability of coverability for static broadcast
networks, one attempt is to introduce non-deterministic reconfiguration of the
communication topology. This solution also allows one to model arbitrary
mobility of the nodes, which is meaningful, _e.g._ for mobile ad-hoc networks
[DSZ10].

Under this semantics, configurations are the same as under the static
semantics. Transitions between configurations however are enhanced by the
ability to modify the communication topology after performing a broadcast.
Formally, from a configuration $\gamma=(\mathsf{N},\mathsf{E},\mathsf{L})$,
there is a step to
$\gamma^{\prime}=(\mathsf{N}^{\prime},\mathsf{E}^{\prime},\mathsf{L}^{\prime})$
if $\mathsf{N}^{\prime}=\mathsf{N}$, and there exists
$\mathsf{n}\in\mathsf{N}$ and $a\in\Sigma$ such that
$(\mathsf{L}(\mathsf{n}),!\textit{a},\mathsf{L}^{\prime}(\mathsf{n}))\in\Delta$,
and for every $\mathsf{n}^{\prime}\in\mathsf{N}$, if
$\mathsf{n}^{\prime}\in\mathsf{Neigh}_{\gamma}(\mathsf{n})$, then
$(\mathsf{L}(\mathsf{n}^{\prime}),?\textit{a},\mathsf{L}^{\prime}(\mathsf{n}^{\prime}))\in\Delta$,
otherwise
$\mathsf{L}^{\prime}(\mathsf{n}^{\prime})=\mathsf{L}(\mathsf{n}^{\prime})$: a
step thus reflects that the communication topology may change from
$\mathsf{E}$ to $\mathsf{E}^{\prime}$ after the broadcast of a message from a
node to its neighbours in the old topology. For such a step, we write
$\gamma\xrightarrow{\mathsf{n},!\textit{a}}_{\mathtt{r}}\gamma^{\prime}$, or
simply $\gamma\to_{\mathtt{r}}\gamma^{\prime}$.

Figure 3 gives an example of a reconfigurable execution for the broadcast
protocol of Figure 1. Note that the communication topology indeed evolves
along the execution. As before, the colored nodes broadcast a message in the
step leading to the next configuration. This sample execution does cover
$\Smiley$.

$q_{0}$$q_{0}$$q_{0}$$\xrightarrow{!\textit{a}}_{\mathtt{r}}$$q_{1}$$q_{0}$$q_{0}$$\xrightarrow{!\textit{b}_{1}}_{\mathtt{r}}$$q_{2}$$r_{1}$$q_{0}$$\xrightarrow{!\textit{a}}_{\mathtt{r}}$$q_{3}$$r_{1}$$q_{0}$$\xrightarrow{!\textit{b}_{2}}_{\mathtt{r}}$$q_{4}$$\Smiley[2]$$q_{0}$

Figure 3. A sample reconfigurable execution for the broadcast protocol from
Figure 1.

Similarly to the static case, we write
$\mathsf{Exec}_{\mathtt{r}}(\mathcal{P})$ and
$\mathsf{COVER}_{\mathtt{r}}(\mathcal{P},F)$ for, respectively the set of all
reconfigurable executions in $\mathcal{P}$, and the set of all reconfigurable
executions in $\mathcal{P}$ that cover $F$. We will also use the same
notations $\textsf{\\#nodes}(\rho)$, $\textsf{\\#steps}(\rho)$ and
$\textsf{\\#steps}(\rho,\mathsf{n})$ as in the static case.

A noticeable property of reconfigurable broadcast networks is the so-called
copycat property. This monotonicity property has already been observed in
[DSTZ12], and it also appears in several other contexts, for instance in
asynchronous shared-memory systems [EGM13].

######  Proposition 1 (Copycat for reconfigurable semantics).

Given
$\rho:\gamma_{0}\to_{\mathtt{r}}\gamma_{1}\cdots\to_{\mathtt{r}}\gamma_{s}$ an
execution, with $\gamma_{s}=(\mathsf{N},\mathsf{E},\mathsf{L})$, for every
$q\in\mathsf{L}(\gamma_{s})$, for every $\mathsf{n}^{q}\in\mathsf{N}$ such
that $\mathsf{L}(\mathsf{n}^{q})=q$, there exists $t\in\mathbb{N}$ and an
execution
$\rho^{\prime}:\gamma^{\prime}_{0}\to_{\mathtt{r}}\gamma_{1}^{\prime}\cdots\to_{\mathtt{r}}\gamma_{t}^{\prime}$
with
$\gamma_{t}^{\prime}=(\mathsf{N}^{\prime},\mathsf{E}^{\prime},\mathsf{L}^{\prime})$
such that $|\mathsf{N}^{\prime}|=|\mathsf{N}|{+}1$, there is an injection
$\iota:\mathsf{N}\to\mathsf{N}^{\prime}$ with for every
$\mathsf{n}\in\mathsf{N}$,
$\mathsf{L}^{\prime}(\iota(\mathsf{n}))=\mathsf{L}(\mathsf{n})$, and for the
extra node
$\mathsf{n}_{\mathsf{fresh}}\in\mathsf{N}^{\prime}\setminus\iota(\mathsf{N})$,
$\mathsf{L}^{\prime}(\mathsf{n}_{\mathsf{fresh}})=q$, and
$\textsf{\\#steps}(\rho^{\prime},\mathsf{n}_{\mathsf{fresh}})=\textsf{\\#steps}(\rho,\mathsf{n}^{q})$.

Intuitively, the new node $\mathsf{n}_{\mathsf{fresh}}$ will copy the moves of
node $\mathsf{n}^{q}$: it performs the same broadcasts (to an empty set of
neighbours) and receives the same messages. More precisely, when
$\mathsf{n}^{q}$ broadcasts in $\rho$, it does so also in $\rho^{\prime}$ and
then we disconnect all the nodes and $\mathsf{n}_{\mathsf{fresh}}$ repeats the
broadcast (no other node is affected because of the disconnection); when
$\mathsf{n}^{q}$ receives a message in $\rho$, we connect
$\mathsf{n}_{\mathsf{fresh}}$ to the same neighbours as $\mathsf{n}^{q}$
(_i.e._ , $\iota(\mathsf{n})\sim^{\prime}\mathsf{n}_{\mathsf{fresh}}$ if and
only if $\mathsf{n}\sim\mathsf{n}^{q}$) so that $\mathsf{n}_{\mathsf{fresh}}$
also receives the same message in $\rho^{\prime}$. Figure 4 illustrates the
copycat property for the reconfigurable semantics. In this example, the
bottom-most node copies the middle node from Figure 3. Notice that in the
final configuration, these two nodes are at $q_{4}$ which is highlighted in
blue.

$q_{0}$$q_{0}$$q_{0}$$q_{0}$$\xrightarrow{!\textit{a}}_{\mathtt{r}}$$q_{1}$$q_{0}$$q_{0}$$q_{1}$$\xrightarrow{!\textit{b}_{1}}_{\mathtt{r}}$$q_{0}$$q_{2}$$r_{1}$$q_{1}$$\xrightarrow{!\textit{b}_{1}}_{\mathtt{r}}$$q_{0}$$q_{2}$$r_{1}$$q_{2}$$\xrightarrow{!\textit{a}}_{\mathtt{r}}$$q_{0}$$q_{3}$$r_{1}$$q_{3}$$\xrightarrow{!\textit{b}_{2}}_{\mathtt{r}}$$q_{0}$$q_{4}$$\Smiley[2]$$q_{3}$$\xrightarrow{!\textit{b}_{2}}_{\mathtt{r}}$$q_{0}$$q_{4}$$\Smiley[2]$$q_{4}$

Figure 4. Illustration of the copycat property for reconfigurable semantics.

Relying on the copycat property, when reconfigurations are allowed, the
coverability problem is decidable and solvable in polynomial time. [[DSTZ12]]
Coverability is in PTIME for reconfigurable broadcast networks. More
precisely, a simple saturation algorithm allows one to compute in polynomial
time, the set of all states that can be covered. Despite this complexity
result, to the best of our knowledge, no bounds on the cutoff or length of
witness executions are stated in the literature.

###  2.3. Broadcast networks with messages losses

Communication failures were studied for broadcast networks, assuming non-
deterministic message losses could happen: when a message is broadcast, some
of the neighbours of the sending node may not receive it [DSZ12]. As observed
by the authors, the coverability problem for such networks easily reduces to
the coverability problem in reconfigurable networks by considering a complete
topology, and message losses are simulated by reconfigurations. Thus, message
losses upon reception are equivalent to reconfiguration of the communication
topology.

We propose an alternative semantics here: when a message is broadcast, it
either reaches all neighbours of the sending node, or none of them. This is
relevant in contexts where broadcasts are performed in an atomic manner and
may fail. In contrast to message losses upon reception, it is not obvious to
simulate arbitrary reconfigurations of the communication topology with such
message losses.

Formally, from a configuration $\gamma=(\mathsf{N},\mathsf{E},\mathsf{L})$,
there is a step to
$\gamma^{\prime}=(\mathsf{N}^{\prime},\mathsf{E}^{\prime},\mathsf{L}^{\prime})$
if $\mathsf{N}^{\prime}=\mathsf{N}$, $\mathsf{E}^{\prime}=\mathsf{E}$ and
there exists $\mathsf{n}\in\mathsf{N}$ and $a\in\Sigma$ such that
$(\mathsf{L}(\mathsf{n}),!\textit{a},\mathsf{L}^{\prime}(\mathsf{n}))\in\Delta$,
and either (a) for every $\mathsf{n}^{\prime}\neq\mathsf{n}$,
$\mathsf{L}^{\prime}(\mathsf{n}^{\prime})=\mathsf{L}(\mathsf{n}^{\prime})$ (no
one has received the message, it has been lost), or (b) if
$\mathsf{n}^{\prime}\in\mathsf{Neigh}_{\gamma^{\prime}}(\mathsf{n})$, then
$(\mathsf{L}(\mathsf{n}^{\prime}),?\textit{a},\mathsf{L}^{\prime}(\mathsf{n}^{\prime}))\in\Delta$,
otherwise
$\mathsf{L}^{\prime}(\mathsf{n}^{\prime})=\mathsf{L}(\mathsf{n}^{\prime})$: a
step thus reflects that the broadcast message may be lost when it is sent. We
write $\gamma\xrightarrow{\mathsf{n},!\textit{a}}_{\mathtt{l}}\gamma^{\prime}$
or simply $\gamma\to_{\mathtt{l}}\gamma^{\prime}$. Similarly to the static and
reconfigurable semantics, $\textsf{\\#nodes}(\rho)$ is the number of nodes in
$\rho$, $\textsf{\\#steps}(\rho)$ is the number of steps, and
$\textsf{\\#steps}(\rho,\mathsf{n})$ is the number of broadcasts (including
lost ones) by node $\mathsf{n}$ along $\rho$; moreover, we write
$\textsf{\\#nonlost\\_steps}(\rho,\mathsf{n})$ for the number of successful
broadcasts by node $\mathsf{n}$ along $\rho$.

For lossy executions, we also use the following notations:
$\mathsf{Exec}_{\mathtt{l}}(\mathcal{P})$ for the set of all lossy executions,
and $\mathsf{COVER}_{\mathtt{l}}(\mathcal{P},F)$ for the set of all lossy
executions that cover $F$. One can naturally associate a reconfigurable
execution to any lossy execution by simulating a lost broadcast by an empty
communication topology. More precisely, a lossy execution with communication
topology $E$ can be transformed into a reconfigurable one in which the
communication topology in each configuration is either $\emptyset$ or $E$,
depending on whether the next broadcast is lost or not. Therefore, with slight
abuse of notation, we write
$\mathsf{Exec}_{\mathtt{l}}(\mathcal{P})\subseteq\mathsf{Exec}_{\mathtt{r}}(\mathcal{P})$.

Figure 5 gives an example of a lossy execution for the broadcast protocol of
Figure 1. Note that the topology is fixed throughout the execution. Yet, in
the third transition, some node performs a lossy broadcast, emphasized in the
figure by the subscript “lost”. As before, the colored nodes broadcast a
message in the step leading to the next configuration.

$q_{0}$$q_{0}$$q_{0}$$q_{0}$$q_{0}$$\xrightarrow{!\textit{a}}_{\mathtt{l}}$$q_{1}$$q_{0}$$q_{0}$$q_{1}$$q_{0}$$\xrightarrow{!\textit{b}_{1}}_{\mathtt{l}}$$q_{2}$$r_{1}$$\bot$$q_{1}$$q_{0}$$\xrightarrow{!\textit{b}_{1}}_{\mathtt{l}}$lost$q_{2}$$r_{1}$$\bot$$q_{2}$$q_{0}$$\xrightarrow{!\textit{a}}_{\mathtt{l}}$$q_{2}$$\bot$$q_{0}$$q_{3}$$r_{1}$$\xrightarrow{!\textit{b}_{2}}_{\mathtt{l}}$$q_{2}$$\bot$$\bot$$q_{4}$$\Smiley[2]$

Figure 5. Example of a lossy execution on the protocol from Figure 1.

##  3\. Tight bounds for reconfigurable and lossy broadcast networks

In this section, we will show tight bounds for the cutoff and the minimal
length of a witness execution for the coverability problem. These hold both
for the reconfigurable and the lossy semantics.

###  3.1. Upper bounds on cutoff and covering length for reconfigurable
networks

In view of providing upper bounds on the cutoff and covering length, we first
refine the polynomial time saturation algorithm of [DSTZ12], which computes
all states that can be covered in the reconfigurable semantics. We then show
that, based on the underlying computation, one can construct small witnesses
for both the reconfigurable and lossy semantics. These small witnesses have
linear number of nodes and quadratic number of steps. While it would be enough
to show the result for the lossy semantics only (since, given a broadcast
protocol $\mathcal{P}$,
$\mathsf{Exec}_{\mathtt{l}}(\mathcal{P})\subseteq\mathsf{Exec}_{\mathtt{r}}(\mathcal{P})$),
for pedagogical reasons, we provide the two proofs, starting with the simplest
one, _i.e._ for reconfigurable semantics.

Let us fix for the rest of this section, a protocol
$\mathcal{P}=(Q,I,\Sigma,\Delta)$. Delzanno _et al._ proposed a polynomial
time saturation algorithm to compute the set of all states that can be covered
under reconfigurable semantics for broadcast networks [DSTZ12]. This algorithm
maintains a set, say $S$, of states that are known to be coverable. Initially,
$S$ is set to $I$. At each iteration, one adds to $S$ all states that can be
covered in one step from $S$. Formally, $S$ is augmented with all
$q^{\prime}\in Q$ such that, either there exists $q\in S$ and $a\in\Sigma$
with $(q,!\textit{a},q^{\prime})\in\Delta$, or there exist $p,q\in S$,
$p^{\prime}\in Q$ and $a\in\Sigma$ such that
$(p,!\textit{a},p^{\prime})\in\Delta$ and
$(q,?\textit{a},q^{\prime})\in\Delta$. In order to derive upper bounds on the
cutoff and covering length, we slightly modify the existing saturation
algorithm to obtain the one presented in Algorithm 1. We augment the
saturation set $S$ by at most one element in each iteration. Additionally, we
associate an integer-valued variable $c$ that counts the number of nodes that
are sufficient to cover the set $S$ at the current iteration. Intuitively,
when a state is added as the target of a broadcast transition, we copy the
node corresponding to the state responsible for the broadcast, whereas in case
of a reception transition we need to copy two nodes involved in the action.

Algorithm 1 Refined saturation algorithm for coverability

1:$S:=I$; $c:=|I|$; $S^{\prime}:=\emptyset$

2:while $S\neq S^{\prime}$ do

3: $S^{\prime}:=S$

4: if $\exists(q_{1},!\textit{a},q_{2})\in\Delta$ s.t. $q_{1}\in S^{\prime}$
and $q_{2}\not\in S^{\prime}$ then

5: $S:=S\cup\\{q_{2}\\}$; $c:=c+1$

6: else if $\exists(q_{1},!\textit{a},q_{2})\in\Delta$ and
$(q^{\prime}_{1},?\textit{a},q^{\prime}_{2})\in\Delta$ s.t.
$q_{1},q_{2},q^{\prime}_{1}\in S^{\prime}$ and $q^{\prime}_{2}\not\in
S^{\prime}$ then

7: $S:=S\cup\\{q^{\prime}_{2}\\}$; $c:=c+2$

8: end if

9:end while

10:return $S$

[[DSTZ12]] Algorithm 1 terminates and the set $S$ the algorithm returns is
exactly the set of coverable states. In particular,
$\mathsf{COVER}_{\mathtt{r}}(\mathcal{P},F)\neq\emptyset$ iff $F\cap
S\neq\emptyset$.

Let $S_{0},S_{1},\ldots,S_{m}$ be the sets after each iteration of the
algorithm, with $S_{0}=I$ and $S_{m}=S$; and $c_{0},c_{1}\ldots,c_{m}$ be the
respective values of the variable $c$ with $c_{0}=|I|$. We fix an ordering on
the states in $S$ on the basis of insertion in $S$: for all $1\leq i\leq m$,
$q_{i}$ is such that $q_{i}\in S_{i}\setminus S_{i-1}$. In the following, we
show the desired upper bounds, proving that there exists an execution of size
$O(n)$ and length $O(n^{2})$ covering at the same time all states of $S_{m}$.

######  Theorem 2.

Let $\mathcal{P}=(Q,I,\Sigma,\Delta)$ be a broadcast protocol, $F\subseteq Q$
and $S$ be the set of states returned by Algorithm 1 on input $\mathcal{P}$.
If $F\cap S\neq\emptyset$, then there exists
$\rho\in\mathsf{COVER}_{\mathtt{r}}(\mathcal{P},F)$ with
$\textsf{\\#nodes}(\rho)\leq 2|Q|$ and $\textsf{\\#steps}(\rho)\leq 2|Q|^{2}$.

Theorem 2 is a consequence of the following lemma.

######  Lemma 3.

For every step $i$ of Algorithm 1, there exists an initial configuration
$\gamma_{0}$, a configuration $\gamma$ and a reconfigurable execution
$\rho:\gamma_{0}\xrightarrow{*}_{\mathtt{r}}\gamma$ such that
$\mathsf{L}(\gamma)=S_{i}$, $\textsf{\\#nodes}(\rho)=c_{i}$, and
$\max_{\mathsf{n}}\textsf{\\#steps}(\rho,\mathsf{n})\leq i$.

######  Proof 3.1.

The lemma is proved by induction on $i$. The base case $i=0$ is obvious: take
the initial configuration $\gamma_{0}$ with $|I|$ nodes, and label each node
with a different initial state; its size is $|I|$, and the length of the
execution is $0$, hence so is the maximum active length.

To prove the induction step, we distinguish two cases: depending on whether
$q_{i+1}$ was added as the target state of a broadcast transition
$q\xrightarrow{!\textit{a}}$ for some $q\in S_{i}$; or whether $q_{i+1}$ is
the target state of a reception from some $q\in S_{i}$ with matching broadcast
between two states already in $S_{i}$.

Case 1: There exists $q\in S_{i}$ with $q\xrightarrow{!\textit{a}}q_{i+1}$. We
apply the induction hypothesis to step $i$, and exhibit an execution
$\rho:\gamma_{0}\xrightarrow{*}_{\mathtt{r}}\gamma$ such that
$\mathsf{L}(\gamma)=S_{i}$, $\textsf{\\#nodes}(\rho)=c_{i}$ and
$\max_{\mathsf{n}}\textsf{\\#steps}(\rho,\mathsf{n})\leq i$. Applying the
copycat property (see Proposition 1), we construct an execution
$\rho^{\prime}:\gamma^{\prime}_{0}\xrightarrow{*}_{\mathtt{r}}\gamma^{\prime}$
such that $\gamma^{\prime}_{0}$ has one node more than $\gamma_{0}$, and,
focusing on the nodes (since we are in a reconfigurable setting, edges in the
configuration are not important), $\gamma^{\prime}$ coincides with $\gamma$,
with an extra node $\mathsf{n}$ labelled by $q$. We then disconnect all nodes
and extend with a transition
$\gamma^{\prime}\xrightarrow{\mathsf{n},!\textit{a}}_{\mathtt{r}}\gamma^{\prime\prime}$,
which makes only progress node $\mathsf{n}$ from $q$ to $q_{i+1}$; the
resulting execution is denoted $\rho^{\prime\prime}$. Then:

  1. (1)

$\mathsf{L}(\gamma^{\prime\prime})=S_{i}\cup\\{q_{i+1}\\}=S_{i+1}$,

  2. (2)

$\textsf{\\#nodes}(\rho^{\prime\prime})=c_{i}+1=c_{i+1}$,

  3. (3)

$\max_{\mathsf{n}}\textsf{\\#steps}(\rho^{\prime\prime},\mathsf{n})\leq\max_{\mathsf{n}}\textsf{\\#steps}(\rho,\mathsf{n})+1\leq
i+1$; Indeed, the active length of the copycat node along $\rho^{\prime}$
coincides with the active length of some existing node along $\rho$, and it is
increased only by $1$ in $\rho^{\prime\prime}$.

This proves the induction step in the first case.

Case 2: There exists $q,q^{\prime},q^{\prime\prime}\in S_{i}$ with
$q\xrightarrow{?\textit{a}}q_{i+1}$ and
$q^{\prime}\xrightarrow{!\textit{a}}q^{\prime\prime}$. The idea is similar to
the previous case, but one should apply the copycat property twice, to both
$q$ and $q^{\prime}$. We formalize this.

We apply the induction hypothesis to step $i$, and exhibit an execution
$\rho:\gamma_{0}\xrightarrow{*}_{\mathtt{r}}\gamma$ such that
$\mathsf{L}(\gamma)=S_{i}$, $\textsf{\\#nodes}(\rho)=c_{i}$ and
$\max_{\mathsf{n}}\textsf{\\#steps}(\rho,\mathsf{n})\leq i$. Applying the
copycat property (see Proposition 1) twice, to both $q$ and $q^{\prime}$, we
construct an execution
$\rho^{\prime}:\gamma^{\prime}_{0}\xrightarrow{*}_{\mathtt{r}}\gamma^{\prime}$
such that $\gamma^{\prime}_{0}$ has two nodes more than $\gamma_{0}$, and,
focusing on the nodes, $\gamma^{\prime}$ coincides with $\gamma$, with one
extra node $\mathsf{n}$ labelled by $q$ and one extra node
$\mathsf{n}^{\prime}$ labelled by $q^{\prime}$. We then connect nodes
$\mathsf{n}$ and $\mathsf{n}^{\prime}$ and disconnect all other nodes, and
extend with a transition
$\gamma^{\prime}\xrightarrow{\mathsf{n}^{\prime},!\textit{a}}_{\mathtt{r}}\gamma^{\prime\prime}$;
this makes node $\mathsf{n}$ progress from $q$ to $q_{i+1}$ and node
$\mathsf{n}^{\prime}$ progress from $q^{\prime}$ to $q^{\prime\prime}$; all
other nodes are unchanged; the resulting execution is denoted
$\rho^{\prime\prime}$. Then:

  1. (1)

$\mathsf{L}(\gamma^{\prime\prime})=S_{i}\cup\\{q^{\prime\prime},q_{i+1}\\}=S_{i+1}$
since $q^{\prime\prime}\in S_{i}$,

  2. (2)

$\textsf{\\#nodes}(\rho^{\prime\prime})=c_{i}+2=c_{i+1}$,

  3. (3)

$\max_{\mathsf{n}}\textsf{\\#steps}(\rho^{\prime\prime},\mathsf{n})\leq\max_{\mathsf{n}}\textsf{\\#steps}(\rho,\mathsf{n})+1\leq
i+1$; Indeed the active length of any of the copycat node along
$\rho^{\prime}$ coincides with the active length of some existing node along
$\rho$, and it is increased by at most $1$ in $\rho^{\prime\prime}$.

This proves the induction step in the second case, and concludes the proof of
the lemma.

To conclude the proof of Theorem 2, we recall that Algorithm 1 is sound and
complete: the output set $S_{m}$ is precisely the set of states that can be
covered. Hence, from Lemma 3, we deduce that if
$\mathsf{COVER}_{\mathtt{r}}(\mathcal{P},F)\neq\emptyset$, then there is
$\rho\in\mathsf{COVER}_{\mathtt{r}}(\mathcal{P},F)$ such that:

  1. (1)

$\mathsf{L}(\gamma)=S_{m}$;

  2. (2)

$\textsf{\\#nodes}(\rho)=c_{m}\leq|I|+2m\leq|I|+2(|Q|-|I|)=2|Q|-|I|$;

  3. (3)

$\max_{\mathsf{n}}\textsf{\\#steps}(\rho,\mathsf{n})\leq m\leq|Q|-|I|$.

Therefore
$\textsf{\\#steps}(\rho)\leq\big{(}\textsf{\\#nodes}(\rho)\big{)}\cdot\Big{(}\max_{\mathsf{n}}\textsf{\\#steps}(\rho,\mathsf{n})\Big{)}\leq
2|Q|^{2}$, so that we established the desired bounds for Theorem 2.

###  3.2. Upper bounds on cutoff and covering length for lossy networks

Perhaps surprisingly, Algorithm 1 also computes the set of states that can be
covered by lossy executions. Concerning coverable states, the reconfigurable
and lossy semantics thus agree. In Section 4, we will show that reconfigurable
covering executions can be linearly more succinct than lossy covering
executions.

######  Lemma 4.

Algorithm 1 returns the set $S$ of coverable states for lossy broadcast
networks. In particular,
$\mathsf{COVER}_{\mathtt{l}}(\mathcal{P},F)\neq\emptyset$ iff $F\cap
S\neq\emptyset$.

Indeed,
$\mathsf{Exec}_{\mathtt{l}}(\mathcal{P})\subseteq\mathsf{Exec}_{\mathtt{r}}(\mathcal{P})$.
Therefore $\mathsf{COVER}_{\mathtt{l}}(\mathcal{P},F)\neq\emptyset$ implies
$\mathsf{COVER}_{\mathtt{r}}(\mathcal{P},F)\neq\emptyset$ and by Lemma 1, we
conclude $F\cap S\neq\emptyset$. The other direction of Lemma 4 is a
consequence of the following theorem.

######  Theorem 5.

Let $\mathcal{P}=(Q,I,\Sigma,\Delta)$ be a broadcast protocol, $F\subseteq Q$
and and $S$ be the set of states returned by Algorithm 1 on input
$\mathcal{P}$. If $F\cap S\neq\emptyset$, then there exists
$\rho\in\mathsf{COVER}_{\mathtt{l}}(\mathcal{P},F)$ with
$\textsf{\\#nodes}(\rho)\leq 2|Q|$ and $\textsf{\\#steps}(\rho)\leq 2|Q|^{2}$.

Before going to the proof of Theorem 5, we show a copycat property for the
lossy broadcast networks, as a counterpart of Proposition 1 for the lossy
semantics. Since the communication topology is static in lossy networks, the
following proposition explicitly relates the communication topologies in the
initial execution and its copycat extension.

######  Proposition 6 (Copycat for lossy semantics).

Given
$\rho:\gamma_{0}\to_{\mathtt{l}}\gamma_{1}\cdots\to_{\mathtt{l}}\gamma_{r}$ an
execution, with $\gamma_{r}=(\mathsf{N},\mathsf{E},\mathsf{L})$, for every
$q\in\mathsf{L}(\gamma_{r})$, for every $\mathsf{n}^{q}\in\mathsf{N}$ such
that $\mathsf{L}(\mathsf{n}^{q})=q$, there exists $s\in\mathbb{N}$ and an
execution
$\rho^{\prime}:\gamma^{\prime}_{0}\to_{\mathtt{l}}\gamma_{1}^{\prime}\cdots\to_{\mathtt{l}}\gamma_{s}^{\prime}$
with
$\gamma_{s}^{\prime}=(\mathsf{N}^{\prime},\mathsf{E}^{\prime},\mathsf{L}^{\prime})$
such that $|\mathsf{N}^{\prime}|=|\mathsf{N}|{+}1$, there is an injection
$\iota:\mathsf{N}\to\mathsf{N}^{\prime}$ with for every
$\mathsf{n}\in\mathsf{N}$,
$\mathsf{L}^{\prime}(\iota(\mathsf{n}))=\mathsf{L}(\mathsf{n})$, and for the
extra node
$\mathsf{n}_{\mathsf{fresh}}\in\mathsf{N}^{\prime}\setminus\iota(\mathsf{N})$,
$\mathsf{L}^{\prime}(\mathsf{n}_{\mathsf{fresh}})=q$, for every
$\mathsf{n}\in\mathsf{N}$,
$\mathsf{n}_{\mathsf{fresh}}\sim^{\prime}\iota(\mathsf{n})$ iff
$\mathsf{n}^{q}\sim\mathsf{n}$,
$\textsf{\\#steps}(\rho^{\prime},\mathsf{n}_{\mathsf{fresh}})=\textsf{\\#steps}(\rho,\mathsf{n}^{q})$,
and
$\textsf{\\#nonlost\\_steps}(\rho^{\prime},\mathsf{n}_{\mathsf{fresh}})=0$.

######  Proof 3.2.

First notice that, from our definition of lossy semantics, the topology should
be the same in $\gamma_{0}$ and in $\gamma_{r}$, hence we can write
$\gamma_{0}=(\mathsf{N},\mathsf{E},\mathsf{L}_{0})$, and more generally, for
every $i$, $\gamma_{i}=(\mathsf{N},\mathsf{E},\mathsf{L}_{i})$. Define
$\mathsf{N}^{\prime}$ as a finite set such that
$|\mathsf{N}^{\prime}|=|\mathsf{N}|+1$, and fix an injection
$\iota:\mathsf{N}\to\mathsf{N}^{\prime}$. Write $\mathsf{n}_{\mathsf{fresh}}$
for the unique element of $\mathsf{N}^{\prime}\setminus\iota(\mathsf{N})$. Set
$\mathsf{L}^{\prime}_{0}(\iota(\mathsf{n}))=\mathsf{L}_{0}(\mathsf{n})$ for
every $\mathsf{n}\in\mathsf{N}$, and
$\mathsf{L}^{\prime}_{0}(\mathsf{n}_{\mathsf{fresh}})=\mathsf{L}_{0}(\mathsf{n}^{q})$.
Define the edge relation $\mathsf{E}^{\prime}$ by its induced edge relation
$\sim^{\prime}$ such that
$\iota(\mathsf{n})\sim^{\prime}\iota(\mathsf{n}^{\prime})$ iff
$\mathsf{n}\sim\mathsf{n}^{\prime}$, and
$\mathsf{n}_{\mathsf{fresh}}\sim^{\prime}\iota(\mathsf{n}^{\prime})$ iff
$\mathsf{n}^{q}\sim\mathsf{n}^{\prime}$.

The idea will then be to make $\mathsf{n}_{\mathsf{fresh}}$ follow what
$\mathsf{n}^{q}$ is doing. Roughly, if $\mathsf{n}^{q}$ is receiving a message
to progress, then we will connect $\mathsf{n}_{\mathsf{fresh}}$ to a relevant
node to also receive the message; if $\mathsf{n}^{q}$ is broadcasting a
message, then we will make $\mathsf{n}_{\mathsf{fresh}}$ broadcast a message
and lose, so that no other node is impacted.

Formally, we will show by induction on $i$ that for every $0\leq i\leq r$,
there is an execution
$\rho^{\prime}_{i}:\gamma^{\prime}_{0}\to_{\mathtt{l}}\gamma^{\prime}_{1}\dots\to_{\mathtt{l}}\gamma^{\prime}_{f(i)}$
for some $f(i)$, such that
$\mathsf{L}^{\prime}_{i}(\iota(\mathsf{n}))=\mathsf{L}_{i}(\mathsf{n})$ for
every $\mathsf{n}\in\mathsf{N}$ and
$\mathsf{L}^{\prime}_{i}(\mathsf{n}_{\mathsf{fresh}})=\mathsf{L}_{i}(\mathsf{n}^{q})$.
The initial case $i=0$ is obvious. We then assume that we have constructed a
relevant $\rho^{\prime}_{i}$ for some $i<r$, and we will extend it to
$\rho^{\prime}_{i+1}$ as follows. We make a case distinction depending on the
nature of the step $\gamma_{i}\to_{\mathtt{l}}\gamma_{i+1}$:

  * •

Assume
$\gamma_{i}\xrightarrow{\mathsf{n},!\textit{a}}_{\mathtt{l}}\gamma_{i+1}$ is a
broadcast message with $\mathsf{n}^{q}\neq\mathsf{n}$, then
$\rho^{\prime}_{i+1}$ is obtained by extending $\rho^{\prime}_{i}$ with the
broadcast
$\gamma^{\prime}_{f(i)}\xrightarrow{\iota(\mathsf{n}),!\textit{a}}\gamma^{\prime}_{f(i)+1}$,
with the condition that it should be lost if and only if it was lost in the
original execution. For checking correctness, we distinguish two cases:

    * –

the broadcast message was not lost, and $\mathsf{n}^{q}\sim\mathsf{n}$. Then,
it is the case that
$\mathsf{n}_{\mathsf{fresh}}\sim^{\prime}\iota(\mathsf{n})$, hence
$\mathsf{n}_{\mathsf{fresh}}$ also receives the message. By resolving properly
the nondeterminism, we can make the label of $\mathsf{n}_{\mathsf{fresh}}$
become the same as the label of $\mathsf{n}^{q}$ in
$\gamma^{\prime}_{f(i)+1}$. Note also that all nodes in $\iota(\mathsf{N})$
can progress to the same states as those of $\mathsf{N}$ in $\gamma_{i+1}$;

    * –

the broadcast message was lost, or $\mathsf{n}^{q}\not\sim\mathsf{n}$, then it
is the case that the label of $\mathsf{n}^{q}$ has not been changed in
$\gamma_{i}\xrightarrow{\mathsf{n},!\textit{a}}_{\mathtt{l}}\gamma_{i+1}$, and
so will the label of the fresh node in $\gamma^{\prime}_{f(i)}$.

  * •

Assume
$\gamma_{i}\xrightarrow{\mathsf{n}^{q},!\textit{a}}_{\mathtt{l}}\gamma_{i+1}$
is a broadcast message, then we extend $\rho^{\prime}_{i}$ with the two steps
$\gamma^{\prime}_{f(i)}\xrightarrow{\iota(\mathsf{n}^{q}),!\textit{a}}\gamma^{\prime}_{f(i)+1}\xrightarrow{\mathsf{n}_{\mathsf{fresh}},!\textit{a}}\gamma^{\prime}_{f(i)+2}$
(resolving nondeterminism in a similar way as in
$\gamma_{i}\xrightarrow{\mathsf{n}^{q},!\textit{a}}_{\mathtt{l}}\gamma_{i+1}$),
and we make the last broadcast lossy whereas the broadcast from
$\iota(\mathsf{n}^{q})$ is lossy if and only if it was lossy in
$\gamma_{i}\to_{\mathtt{l}}\gamma_{i+1}$.

This concludes the induction. Notice that in the constructed execution, node
$\mathsf{n}_{\mathsf{fresh}}$ does not make any real sending.

For any configuration $\gamma=(\mathsf{N},\mathsf{E},\mathsf{L})$ and a node
$\mathsf{n}$, we write $\mathsf{L}(\mathsf{n})=\times$ if $\mathsf{n}$ is not
important anymore in the execution, in other words all the required conditions
in $\gamma^{\prime}$ such that
$\gamma\xrightarrow{*}_{\mathtt{l}}\gamma^{\prime}$ are still satisfied
whatever $\mathsf{L}(\mathsf{n})$ is.

Recall the notations introduced to study the saturation algorithm:
$S_{0}=I,S_{1},\ldots,S_{m}=S$ are the sets after each iteration; $c_{i}$ is
the value of the variable $c$ after iteration $i$; and $q_{i}$ is the state
such that $q_{i}\in S_{i}\setminus S_{i-1}$ for all $1\leq i\leq m$. We will
refine the construction from the proof of Lemma 3 (in the context of
reconfigurable broadcast networks), and build inductively a lossy execution
covering all states in $S_{i}$. Since the topology is static, some nodes which
have “finished their jobs” will remain connected to other nodes, and may
therefore continue to change states (contrary to Lemma 3 where they could be
fully disconnected). Hence, in every such execution, every state $q\in S_{i}$
(which is then covered by the execution) will have a main corresponding node,
whose label will remain $q$. All nodes which are not the main node of a state
will be assigned $\times$, since their labels will become meaningless.

We formalize this idea in the lemma below. However, for better understanding,
we also illustrate this inductive construction of a witness execution in
Figure 7 on the simple broadcast protocol from Figure 6. Configurations are
represented vertically: they involve 10 nodes, and the communication topology
is given for the first configuration only, for the sake of readability. To
save space, several broadcasts (of the same message type, from different
nodes) may happen in a _macrostep_ that merges several steps. This is for
instance the case in the first macrostep, where $a$ is being broadcast from
the node in set $S_{1}$, as well as from the first node in set $S_{2}$. Dashed
arrows are used to represent that a node is not involved in some macrostep and
thus stays in the same state. In the execution, the nodes that are performing
a real broadcast are colored yellow, the ones which change their state upon
reception of a message are colored gray, and blue nodes indicate the main
nodes for the coverable states.

$\scriptstyle q_{0}$$\scriptstyle q_{1}$$\scriptstyle q_{2}$$\scriptstyle
q_{3}$$\scriptstyle q_{4}$$\scriptstyle q_{5}$$\scriptstyle
q_{6}$$\scriptstyle!\textit{a}$$\scriptstyle?\textit{a}$$\scriptstyle!\textit{b}$$\scriptstyle?\textit{b}$$\scriptstyle!\textit{c}$$\scriptstyle?\textit{c}$
Figure 6. Illustrating example for the saturation algorithm.

$S_{0}$$S_{1}$$S_{2}$$S_{3}$$S_{4}$$S_{5}$$S_{6}$$\gamma_{0}$$\gamma_{1}$$\cdots\cdots$$\gamma_{n}$$q_{0}$$q_{0}$$q_{0}$$q_{0}$$q_{0}$$q_{0}$$q_{0}$$q_{0}$$q_{0}$$q_{0}$$q_{1}$$\times$$q_{2}$$q_{2}$$q_{2}$$q_{0}$$q_{0}$$q_{0}$$q_{2}$$q_{2}$$q_{2}$$q_{1}$$q_{1}$$q_{1}$$q_{2}$$q_{3}$$\times$$q_{4}$$q_{4}$$q_{4}$$q_{2}$$q_{4}$$q_{4}$$q_{3}$$q_{5}$$\times$$q_{6}$$q_{0}$$q_{1}$$\times$$q_{2}$$q_{3}$$\times$$q_{4}$$!\textit{a}$lost$!\textit{a}$$?\textit{a}$$?\textit{a}$$?\textit{a}$$!\textit{a}$lost$!\textit{a}$lost$!\textit{a}$lost$?\textit{a}$$!\textit{b}$lost$!\textit{b}$lost$!\textit{b}$$?\textit{b}$$?\textit{b}$$?\textit{b}$$!\textit{c}$lost$!\textit{c}$$?\textit{c}$

Figure 7. Lossy covering execution from the saturation algorithm on the
protocol in Figure 6. Configurations are represented vertically; for
readability, macrosteps merge several broadcasts.

######  Lemma 7.

For every step $i$ of the refined saturation algorithm, there exists a
configuration $\gamma=(\mathsf{N},\mathsf{E},\mathsf{L})$ and an execution
$\rho:\gamma_{0}\xrightarrow{*}_{\mathtt{l}}\gamma$ such that:

  * •

$\mathsf{L}(\gamma)\setminus\\{\times\\}=S_{i}$ and
$\textsf{\\#nodes}(\rho)=c_{i}$,

  * •

$\max_{\mathsf{n}}\textsf{\\#steps}(\rho,\mathsf{n})\leq i$ and
$\max_{\mathsf{n}}\textsf{\\#nonlost\\_steps}(\rho,\mathsf{n})\leq 1$,

  * •

for every $q\in S_{i}$, there exists
$\mathsf{n}^{\mathsf{main}}_{q}\in\mathsf{N}$ such that

    * –

$\mathsf{L}(\mathsf{n}^{\mathsf{main}}_{q})=q$ and
$\textsf{\\#nonlost\\_steps}(\rho,\mathsf{n}^{\mathsf{main}}_{q})=0$,

    * –

$\mathsf{n}^{\mathsf{main}}_{q}\sim\mathsf{n}$ implies
$\mathsf{L}(\mathsf{n})=\times$, and if
$\mathsf{n}\notin\\{\mathsf{n}^{\mathsf{main}}_{q}\mid q\in S_{i}\\}$, then
$\mathsf{L}(\mathsf{n})=\times$.

######  Proof 3.3.

We do the proof by induction on $i$. The case $i=0$ is obvious, by picking one
main node per initial state in $I$, and by disconnecting all nodes; hence
forming an initial configuration satisfying all the requirements.

To prove the induction step, we distinguish two cases: depending on whether
$q_{i+1}$ was added as the target state of a broadcast action $!\textit{a}$
from some $q\in S_{i}$; or whether $q_{i+1}$ is the target state of a
reception from some $q\in S_{i}$ with matching broadcast between two states
already in $S_{i}$.

Case 1: There exists $q\in S_{i}$ with $q\xrightarrow{!\textit{a}}q_{i+1}$. We
apply the induction hypothesis to step $i$, and exhibit the various elements
of the statement. Applying the copycat property for lossy broadcast systems
(that is, Proposition 6) with node $\mathsf{n}^{\mathsf{main}}_{q}$, we build
an execution
$\rho^{\prime}:\gamma^{\prime}_{0}\xrightarrow{*}_{\mathtt{l}}\gamma^{\prime}$
such that $\gamma^{\prime}=(\mathsf{N},\mathsf{E},\mathsf{L}^{\prime})$ with
$|\mathsf{N}^{\prime}|=|\mathsf{N}|+1$, and an appropriate injection $\iota$.
The fresh node $\mathsf{n}_{\mathsf{fresh}}$ is connected to nodes to which
$\mathsf{n}^{\mathsf{main}}_{q}$ was connected before; hence, by induction
hypothesis, it is only connected to nodes labelled with $\times$. Then we
extend $\rho^{\prime}$ with
$\gamma^{\prime}\xrightarrow{\mathsf{n}_{\mathsf{fresh}},!\textit{a}}\gamma^{\prime\prime}$
and lose the message (this is for condition
$\textsf{\\#nonlost\\_steps}(\rho,\mathsf{n}^{\mathsf{main}}_{q})=0$ to be
satisfied). We declare
$\mathsf{n}^{\mathsf{main}}_{q_{i+1}}=\mathsf{n}_{\mathsf{fresh}}$. All
requirements for $\gamma^{\prime\prime}$ are easily checked to be satisfied
(when a node is labelled with $\times$ in $\gamma^{\prime}$, then it remains
labelled by $\times$ in $\gamma^{\prime\prime}$).

Case 2: There exist $q,q^{\prime},q^{\prime\prime}\in S_{i}$ such that
$q\xrightarrow{?\textit{a}}q_{i+1}$ and
$q^{\prime}\xrightarrow{!\textit{a}}q^{\prime\prime}$. We apply the induction
hypothesis to step $i$, and exhibit the various elements of the statement.
Applying twice the copycat property (that is, Proposition 6), once with node
$\mathsf{n}^{\mathsf{main}}_{q}$ and once with node
$\mathsf{n}^{\mathsf{main}}_{q^{\prime}}$, we build an execution
$\rho^{\prime}:\gamma^{\prime}_{0}\xrightarrow{*}_{\mathtt{l}}\gamma^{\prime}$
such that $\gamma^{\prime}=(\mathsf{N},\mathsf{E},\mathsf{L}^{\prime})$ with
$|\mathsf{N}^{\prime}|=|\mathsf{N}|+2$, and an appropriate injection $\iota$.
The two fresh nodes $\mathsf{n}_{\mathsf{fresh}}$ and
$\mathsf{n}^{\prime}_{\mathsf{fresh}}$ are only connected to $\times$-nodes in
$\gamma^{\prime}$ (by induction hypothesis on $\mathsf{n}^{\mathsf{main}}_{q}$
and $\mathsf{n}^{\mathsf{main}}_{q^{\prime}}$ respectively). We transform
$\gamma^{\prime}_{0}$ into $\gamma^{\prime\prime}_{0}$ by connecting the two
nodes $\mathsf{n}_{\mathsf{fresh}}$ and
$\mathsf{n}^{\prime}_{\mathsf{fresh}}$. By Proposition 6, we know that those
two nodes do not perform any real sending (_i.e._ ,
$\textsf{\\#nonlost\\_steps}(\rho^{\prime},\mathsf{n}_{\mathsf{fresh}})=0$ and
$\textsf{\\#nonlost\\_steps}(\rho^{\prime},\mathsf{n}_{\mathsf{fresh}}^{\prime})=0$),
hence this new connection will not affect the labels of the nodes, and we can
safely apply the same transitions as in $\rho^{\prime}$ from
$\gamma^{\prime\prime}_{0}$ to get an execution
$\rho^{\prime\prime}:\gamma^{\prime\prime}_{0}\xrightarrow{*}_{\mathtt{l}}\gamma^{\prime\prime}$,
where $\gamma^{\prime\prime}$ coincides with $\gamma^{\prime}$, with an extra
connection between nodes $\mathsf{n}_{\mathsf{fresh}}$ and
$\mathsf{n}^{\prime}_{\mathsf{fresh}}$. Then, we extend $\rho^{\prime\prime}$
with
$\gamma^{\prime\prime}\xrightarrow{\mathsf{n}^{\prime}_{\mathsf{fresh}},!\textit{a}}\gamma^{\prime\prime\prime}$.
We assume it is a real sending, hence: node $\mathsf{n}_{\mathsf{fresh}}$ can
progress from state $q$ to $q_{i+1}$, and node
$\mathsf{n}^{\prime}_{\mathsf{fresh}}$ can progress from $q^{\prime}$ to
$q^{\prime\prime}$. All other nodes which are connected to
$\mathsf{n}^{\prime}_{\mathsf{fresh}}$ are labelled by $\times$ in
$\gamma^{\prime\prime}$, hence cannot be really affected by that sending. We
relabel $\mathsf{n}^{\prime}_{\mathsf{fresh}}$ to $\times$, and declare
$\mathsf{n}_{q_{i+1}}^{\mathsf{main}}=\mathsf{n}_{\mathsf{fresh}}$. The
expected conditions of the statement are easily checked to be satisfied by
this new execution.

To conclude the proof of Theorem 5, we perform the same computations as in the
reconfigurable case and obtain the desired bounds on the cutoff and covering
length.

###  3.3. Matching lower bounds for reconfigurable and lossy networks

In this section, we show that the linear bound on the cutoff and the quadratic
bound on the length of witness executions are tight, both for the
reconfigurable and the lossy broadcast networks.

######  Theorem 8.

There exists a family of broadcast protocols ${(\mathcal{P}_{n})}_{n}$ with
$\mathcal{P}_{n}=(Q_{n},I_{n},\Sigma_{n},\Delta_{n})$, and target states
$F_{n}\subseteq Q_{n}$ with $|Q_{n}|\in O(n)$, such that for every $n$,
$\mathsf{COVER}_{\mathtt{r}}(\mathcal{P}_{n},F_{n})\neq\emptyset$,
$\mathsf{COVER}_{\mathtt{l}}(\mathcal{P}_{n},F_{n})\neq\emptyset$, and any
witness reconfigurable or lossy execution has size $O(n)$ and length
$O(n^{2})$.

######  Proof 3.4.

Consider $\mathcal{P}_{n}$, as depicted in Figure 8 with $2n{+}1$ states and
$F_{n}=\\{\Smiley\\}$. Any covering reconfigurable execution involves at least
$n{+}1$ nodes, and has at least $\frac{n^{2}{+}5n}{2}$ steps. Indeed, to reach
, all the $b_{i}$’s have to be broadcast at least once and the node
responsible for the last broadcast of $b_{i}$ stays forever in state $q_{i}$.
An additional node must reach , so that, at least $n{+}1$ nodes are required.
In the minimal covering execution, there will be exactly one node in each
$q_{i}$. Moreover, at least $n{+}2{-}i$ broadcasts of $a_{i}$ need to happen
in addition to a broadcast of each of the $b_{i}$’s. As a consequence, the
covering length in reconfigurable semantics is at least
$n+\sum_{i=1}^{n}(n{+}2{-}i)=n+n^{2}+2n-\frac{n(n{+}1)}{2}=\frac{n^{2}{+}5n}{2}$.
Since any lossy execution can also be seen as a reconfigurable one (where the
lossy broadcast corresponds to a reconfiguration which disconnects all the
nodes), this also provides a similar asymptotic lower bound on the covering
length for lossy networks.

$\scriptstyle q_{0}$$\scriptstyle q_{1}$$\scriptstyle q_{2}$$\scriptstyle
q_{3}$$\scriptstyle
q_{4}$$\scriptstyle\cdots$$\scriptstyle\Smiley[2]$$\scriptstyle!\textit{a}_{1}$$\scriptstyle?\textit{b}_{1}$$\scriptstyle!\textit{a}_{2}$$\scriptstyle?\textit{b}_{2}$$\scriptstyle!\textit{a}_{n}$$\scriptstyle?\textit{b}_{n}$$\scriptstyle!\textit{b}_{1}$$\scriptstyle!\textit{b}_{2}$$\scriptstyle!\textit{b}_{n}$
Figure 8. Broadcast protocol with linear cutoff and quadratic covering length.

##  4\. Succinctness of reconfigurations compared to losses

Until now, reconfigurable and lossy semantics enjoy the same properties: their
coverability problem is decidable, and for positive instances of the
coverability problem, the same tight bounds on cutoff and covering length
hold. We now show that reconfigurable executions can be linearly more succinct
than lossy executions, in terms of number of nodes. Given the tight linear
bound on cutoff, this is somehow optimal.

######  Theorem 9.

There exists a family of broadcast protocols ${(\mathcal{P}_{n})}_{n}$ with
$\mathcal{P}_{n}=(Q_{n},I_{n},\Sigma_{n},\Delta_{n})$ and target states
$F_{n}\subseteq Q_{n}$ such that for every $n$:

  * •

there exists a reconfigurable covering execution in $\mathcal{P}_{n}$with $3$
nodes; and

  * •

any lossy covering execution in $\mathcal{P}_{n}$ requires $O(n)$ nodes.

$\scriptstyle q_{0}$$\scriptstyle q_{1}$$\scriptstyle q_{2}$$\scriptstyle
q_{3}$$\scriptstyle q_{4}$$\scriptstyle\cdots$$\scriptstyle
q_{2n}$$\scriptstyle r_{1}$$\scriptstyle\bot$$\scriptstyle
r_{2}$$\scriptstyle\cdots$$\scriptstyle\Smiley[2]$$\scriptstyle!\textit{a}$$\scriptstyle?\textit{a}$$\scriptstyle!\textit{b}_{1}$$\scriptstyle?\textit{a}$$\scriptstyle!\textit{b}_{2}$$\scriptstyle?\textit{a}$$\scriptstyle!\textit{b}_{n}$$\scriptstyle?\textit{b}_{1}$$\scriptstyle?\textit{b}_{2}$$\scriptstyle?\textit{b}_{n}$$\scriptstyle?\textit{b}_{i}$
Figure 9. Example where reconfigurable semantics needs less nodes than lossy
semantics.

######  Proof 4.1.

$\mathcal{P}_{n}$ is depicted in Figure 9. It has $3n{+}2$ states and we let
$F_{n}=\\{\Smiley\\}$. A covering reconfigurable execution of size 3 is given
in Figure 10. Colored nodes broadcast a message in the step leading to the
next configuration. Along that execution, the top node always remains at
$q_{0}$ and alternatively broadcasts $a$ to the middle node and disconnects;
the middle node follows the chain of $q_{i}$ states and alternatively
broadcasts $b_{i}$’s to the bottom node which gradually progresses along the
chain of states $r_{i}$ and reaches $\Smiley$.

$q_{0}$$q_{0}$$q_{0}$$\xrightarrow{!\textit{a}}_{\mathtt{r}}$$q_{1}$$q_{0}$$q_{0}$$\xrightarrow{!\textit{b}_{1}}_{\mathtt{r}}$$q_{2}$$r_{1}$$q_{0}$$\xrightarrow{!\textit{a}}_{\mathtt{r}}$$q_{3}$$r_{1}$$q_{0}$$\xrightarrow{!\textit{b}_{2}}_{\mathtt{r}}$$\cdots$$\xrightarrow{!\textit{b}_{n}}_{\mathtt{r}}$$q_{2n}$$\Smiley[2]$$q_{0}$

Figure 10. Covering reconfigurable execution with 3 nodes on the protocol from
Figure 9.

Let us argue that in the lossy semantics, $O(n)$ nodes are needed to cover
$\Smiley$. Obviously, one node, say $\mathsf{n}_{\Smiley}$, is needed to reach
the target state, after having received sequentially all the $b_{i}$’s (which
should then correspond to real broadcasts). Towards a contradiction, assume
there is a node $\mathsf{n}$ which makes $\mathsf{n}_{\Smiley}$ progress
twice, that is, $\mathsf{n}$ is connected to $\mathsf{n}_{\Smiley}$ and
performs at least two real broadcasts, say $!\textit{b}_{i}$ and
$!\textit{b}_{j}$ with $i<j$. Node $\mathsf{n}$ needs to receive $j-i>0$ times
the message $a$ after the real $!\textit{b}_{i}$ has occurred, hence there
must be at least one node in state $q_{0}$ connected to $\mathsf{n}$ after the
real $!\textit{b}_{i}$ by $\mathsf{n}$. This is not possible, since this node
has received the real $!\textit{b}_{i}$ while being in $q_{0}$, leading to
$\bot$ if $i>1$, otherwise $\bot$ or $r_{1}$. Hence, each broadcast
$!\textit{b}_{i}$ needs to be sent by a different node. This requires at least
$n{+}1$ nodes, say $\\{\mathsf{n}_{i}\mid 1\leq i\leq
n\\}\cup\\{\mathsf{n}_{\Smiley}\\}$: node $\mathsf{n}_{i}$ is responsible for
broadcasting (with no loss) $b_{i}$ and $\mathsf{n}_{\Smiley}$ progresses
towards $\Smiley$. Notice that $\mathsf{n}_{\Smiley}$ might be the node
responsible for broadcasting all the $a$’s. We conclude that $n{+}1$ is a
lower bound on the number of nodes needed to cover $\Smiley$ in the lossy
semantics.

To complete this example, observe that $n{+}1$ nodes do actually suffice in
lossy semantics to cover $\Smiley$. Let $\mathsf{N}=\\{\mathsf{n}_{i}\mid
1\leq i\leq n\\}\cup\\{\mathsf{n}_{\Smiley}\\}$ and consider the static
communication topology defined by $\mathsf{n}_{i}\sim\mathsf{n}_{\Smiley}$ for
every $i$. In the covering lossy execution, node $\mathsf{n}_{\Smiley}$
initially broadcasts $a$’s, so that all its neighbours, the $\mathsf{n}_{i}$’s
can move to $q_{2i-1}$, using lost sendings. Then each node $\mathsf{n}_{i}$
broadcasts its message $b_{i}$ to $\mathsf{n}_{\Smiley}$, starting with
$\mathsf{n}_{1}$ until $\mathsf{n}_{n}$, so that $\mathsf{n}_{\Smiley}$
reaches $\Smiley$.

$q_{0}$$q_{0}$$q_{0}$$q_{0}$$\cdots$$q_{0}$$\xrightarrow{!\textit{a}}_{\mathtt{l}}$$q_{0}$$q_{1}$$q_{1}$$q_{1}$$\cdots$$q_{1}$$\bigl{(}\xrightarrow{!\textit{b}_{1}}_{\mathtt{l}}\bigr{)}^{n-1}$lost$q_{0}$$q_{1}$$q_{2}$$q_{2}$$\cdots$$q_{2}$$\xrightarrow{!\textit{a}}_{\mathtt{l}}$$q_{0}$$q_{1}$$q_{3}$$q_{3}$$\cdots$$q_{3}$$\bigl{(}\xrightarrow{!\textit{b}_{2}}_{\mathtt{l}}\bigr{)}^{n-2}$lost$q_{0}$$q_{1}$$q_{3}$$q_{4}$$\cdots$$q_{4}$$\cdots$$q_{0}$$q_{1}$$q_{3}$$q_{5}$$\cdots$$q_{2n-1}$$\xrightarrow{!\textit{b}_{1}}_{\mathtt{l}}$$r_{1}$$q_{2}$$q_{3}$$q_{5}$$\cdots$$q_{2n-1}$$\xrightarrow{!\textit{b}_{2}}_{\mathtt{l}}$$\cdots$$\xrightarrow{!\textit{b}_{n}}_{\mathtt{l}}$$\Smiley[2]$$q_{2}$$q_{4}$$q_{6}$$\cdots$$q_{2n}$

Figure 11. A covering lossy execution on the protocol from Figure 9.

Figure 11 depicts the above-decribed lossy execution with $n{+}1$ nodes. In
this picture yellow nodes perform real broadcasts, light blue nodes perform
lossy broadcasts and gray nodes change state upon reception of a message in
the next transition.

##  5\. Complexity of deciding the size of minimal witnesses

We now consider the following decision problem of determining the minimal size
of coverability witnesses for both the reconfigurable and lossy semantics.

Minimum number of nodes for coverability (MinCover) Input: A broadcast
protocol $\mathcal{P}$, a set of states $F\subseteq Q$, and $k\in\mathbb{N}$.
Question: Does there exist a reconfigurable/lossy execution $\rho$ covering
some state in $F$, and with $\textsf{\\#nodes}(\rho)=k$?

By the copycat properties (for both semantics), if there is a covering
execution of size less than $k$, then there is one of size exactly $k$.

######  Theorem 10.

MinCover is NP-complete for both reconfigurable and lossy broadcast networks.

The NP-hardness of MinCover is proved by reduction from SetCover, which is
known to be NP-complete [Kar72]. Recall that SetCover takes as input a finite
set of elements $\mathcal{U}$, a collection $\mathcal{S}$ of subsets of
$\mathcal{U}$ and an integer $k$, and returns yes iff there exists a
subcollection of $\mathcal{S}$ of size at most $k$ that covers $\mathcal{U}$.

######  Lemma 11.

SetCover reduces to MinCover in logarithmic space.

######  Proof 5.1.

Given an instance of the SetCover problem $(\mathcal{U,S},k)$, let us explain
how to construct in logarithmic space, a protocol $\mathcal{P}$ with a set of
target states $F$ and some integer $k^{\prime}$ such that $(\mathcal{U,S},k)$
is a positive instance of SetCover if and only if $(\mathcal{P},F,k^{\prime}$)
is a positive instance of MinCover.

For $\mathcal{U}=\\{a_{1},a_{2},\ldots,a_{n}\\}$ and
$\mathcal{S}=\\{S_{1},S_{2},\ldots,S_{m}\\}$, we define the protocol
$\mathcal{P}=(Q,I,\Sigma,\Delta)$ (depicted in Figure 12) as follows:

  * •

$Q=\\{s_{1},s_{2},\ldots,s_{m}\\}\uplus\\{q_{1},q_{2},\ldots,q_{n}\\}\uplus\\{\Smiley\\}$;

  * •

$I=\\{s_{1},s_{2},\ldots,s_{m}\\}\cup\\{q_{1}\\}$;

  * •

$\Sigma=\mathcal{U}$;

  * •

$\Delta=\\{(s_{j},!\textit{a},s_{j})\ |\ a\in S_{j},1\leq j\leq
m\\}\cup\\{(q_{i},?\textit{a}_{i},q_{i+1})\ |\ 1\leq
i<n\\}\cup\\{(q_{n},?\textit{a}_{n},\Smiley)\\}$;

We further let $F=\\{\Smiley\\}$, and $k^{\prime}=k+1$. Clearly this reduction
can be done in logarithmic space. It remains to show that $\mathcal{U,S}$ has
a cover of size $k$ if and only if there exists a reconfigurable/lossy
execution for $\mathcal{P}$ covering $F$ and with $k^{\prime}$ nodes.

$\scriptstyle s_{1}$$\scriptstyle s_{2}$$\scriptstyle\ldots$$\scriptstyle
s_{m}$$\scriptstyle q_{1}$$\scriptstyle q_{2}$$\scriptstyle
q_{3}$$\scriptstyle\cdots$$\scriptstyle
q_{n}$$\scriptstyle\Smiley[2]$$\scriptstyle!\textit{a}_{11},!\textit{a}_{12},\cdots$$\scriptstyle!\textit{a}_{21},!\textit{a}_{22},\cdots$$\scriptstyle!\textit{a}_{m1},!\textit{a}_{m2},\cdots$$\scriptstyle?\textit{a}_{1}$$\scriptstyle?\textit{a}_{2}$$\scriptstyle?\textit{a}_{3}$$\scriptstyle?\textit{a}_{n}$
Figure 12. Illustration of the reduction to prove NP-hardness of MinCover.

Suppose the SetCover instance is positive, and
$\mathcal{C}=\\{S^{\prime}_{1},\dots,S^{\prime}_{k}\\}$ is a cover. Let us
build a _static_ execution $\rho$ (with no message losses) that covers $F$ in
$\mathcal{P}$. Of course, $\rho$ is also a reconfigurable/lossy execution.
Choose $\gamma_{0}=(\mathsf{N},\mathsf{E},\mathsf{L}_{0})$ where
$\mathsf{N}=\\{\mathsf{n}_{1},\ldots,\mathsf{n}_{k}\\}\cup\\{\mathsf{n}\\}$,
$\mathsf{L}_{0}(\mathsf{n})=q_{1}$,
$\mathsf{L}_{0}(\mathsf{n}_{i})=s_{i}^{\prime}$ for all $1\leq i\leq k$
(assuming $s^{\prime}_{i}=s_{j}$ if $S^{\prime}_{i}=S_{j}$). Since
$\mathcal{C}$ covers each $a_{i}\in\mathcal{U}$, there exists $j$ such that
$a_{i}\in S_{j}^{\prime}$. Thus the broadcast transition
$(s_{j}^{\prime},!\textit{a}_{i},s_{j}^{\prime})$ will be enabled, and some
node may fire the corresponding reception transition
$(q_{i},?\textit{a}_{i},q_{i+1})$ to happen. As for the static communication
topology, it is sufficient to assume that $\mathsf{n}_{j}\sim\mathsf{n}$ for
all $1\leq j\leq k$. Messages $a_{i}$ are being broadcast one after the one,
so that we reach a configuration $\gamma=(\mathsf{N},\mathsf{E},\mathsf{L})$
such that $\mathsf{L}(\mathsf{n})=\Smiley$.

Assume now, that the SetCover instance is negative, thus there is no cover of
size $k$. For a contradiction, assume there exists an initial configuration
$\gamma_{0}=(\mathsf{N},\mathsf{E}_{0},\mathsf{L}_{0})$ of size $k{+}1$ and a
reconfigurable (resp. lossy) execution $\rho$ from $\gamma_{0}$ that covers
$\Smiley$. A necessary condition is that $q_{1}\in\mathsf{L}_{0}(\gamma_{0})$
and a single such node is sufficient, so we let
$\mathsf{N}=\\{\mathsf{n}_{1},\dots,\mathsf{n}_{k},\mathsf{n}\\}$ with
$\mathsf{L}_{0}(\mathsf{n})=q_{1}$,
$\mathsf{L}_{0}(\mathsf{n}_{j})=s_{j}^{\prime}$ for some $s_{j}^{\prime}$
where $1\leq j\leq k$. Since the instance is negative, there exists
$a_{i}\in\mathcal{U}$ such that $a_{i}\notin\bigcup_{1\leq j\leq
k}S_{j}^{\prime}$. Therefore, none of the nodes will be able to broadcast the
message $a_{i}$ and the corresponding reception
$(q_{i},?\textit{a}_{i},q_{i+1})$ will never be performed. This contradicts
the fact that $\rho$ covers $\Smiley$.

For the NP-membership, it suffices to observe that the length of a minimal
covering execution is polynomially bounded, thanks to Theorem 2 and 5,
respectively. Moreover, configurations and updates of configurations by given
transitions can be represented in and computed in a compact way. It is thus
possible to implement a guess-and-check non-deterministic polynomial time
algorithm for the MinCover problem, that non deterministically guesses an
execution with $k$ nodes of maximal length that is polynomially bounded in the
size of the broadcast protocol.

##  6\. Conclusion

In this paper, we have given a tight linear bound on the cutoff and a tight
quadratic bound on the covering length for reconfigurable broadcast networks.
We have also proposed a new semantics for broadcast networks with a static
topology, where messages can be lost at sending. Similar tight bounds can be
proven for that new semantics. Proofs are based on a refinement of the
saturation algorithm of [DSTZ12], and on fine analysis of copycat lemmas. As a
side result of these constructions, we get that the set of states which can be
covered by the two semantics is actually the same, but that the reconfigurable
semantics can be linearly more succinct (in terms of number of nodes). We also
prove the NP-completeness for the existence of a witness execution with the
minimal number of nodes.

As future work, we propose to investigate the tradeoff between number of nodes
and length of covering computation. The family of broadcast protocols
represented in Figure 13 illustrates this phenomenon.

$\scriptstyle q_{0}$$\scriptstyle q_{1}$$\scriptstyle
q_{2}$$\scriptstyle\cdots$$\scriptstyle
q_{n}$$\scriptstyle!\textit{a}$$\scriptstyle?\textit{a}$$\scriptstyle?\textit{a}$$\scriptstyle?\textit{a}$$\scriptstyle!\textit{b}_{i}$$\scriptstyle
r_{1}$$\scriptstyle\cdots$$\scriptstyle\Smiley[1.8]$$\scriptstyle?\textit{b}_{1}$$\scriptstyle?\textit{b}_{n}$
Figure 13. Tradeoff between cutoff and covering length: constant number of
nodes need quadratic length, whereas linear number of nodes only require
linear length.

For instance under the static topology semantics, 3 nodes are necessary and
sufficient to cover $\Smiley$, independently of the value of $n$. However,
with $3$ nodes, the length of any covering execution is quadratic in $n$: one
node performs the broadcasts of all $b_{i}$’s and needs to go $n$ times
through the sequence of states $q_{0},\cdots,q_{n}$. In constrast, with a
linear number of nodes (precisely $n{+}2$), there exists a static covering
execution of linear length. One node sends all others to $q_{n}$ broadcasting
$n$ $a$’s, and then $n$ successive broadcasts of $b_{1}$ to $b_{n}$ are
sufficient to cover $\Smiley$. The precise interplay between number of nodes
and length of covering execution is a possible direction for future work.
Another possible research direction is to investigate the notions of cutoff
and covering length in quantative extensions of broadcast networks, such as
probabilistic protocols [BFS14] or timed networks [ADR+11].

## References

  * [ADR+11] Parosh Aziz Abdulla, Giorgio Delzanno, Othmane Rezine, Arnaud Sangnier, and Riccardo Traverso.  On the verification of timed ad hoc networks.  In Proceedings of the 9th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS’11), volume 6919 of Lecture Notes in Computer Science, pages 256–270. Springer, September 2011.
  * [BFS14] Nathalie Bertrand, Paulin Fournier, and Arnaud Sangnier.  Playing with probabilities in reconfigurable broadcast networks.  In Proceedings of the 17th International Conference on Foundations of Software Science and Computation Structure (FoSSaCS’14), volume 8412 of Lecture Notes in Computer Science, pages 134–148. Springer, April 2014.
  * [BJK+15] Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, and Josef Widder.  Decidability of Parameterized Verification.  Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, 2015.
  * [DSTZ12] Giorgio Delzanno, Arnaud Sangnier, Riccardo Traverso, and Gianluigi Zavattaro.  On the complexity of parameterized reachability in reconfigurable broadcast networks.  In Proceedings of the 32nd Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’12), volume 18 of Leibniz International Proceedings in Informatics, pages 289–300. Leibniz-Zentrum für Informatik, December 2012\.
  * [DSZ10] Giorgio Delzanno, Arnaud Sangnier, and Gianluigi Zavattaro.  Parameterized verification of ad hoc networks.  In Proceedings of the 21st International Conference on Concurrency Theory (CONCUR’10), volume 6269 of Lecture Notes in Computer Science, pages 313–327. Springer, September 2010.
  * [DSZ12] Giorgio Delzanno, Arnaud Sangnier, and Gianluigi Zavattaro.  Verification of ad hoc networks with node and communication failures.  In Proceedings of the 32nd International Conference on Formal Techniques for Distributed Systems (FMOODS/FORTE’12), volume 7273 of Lecture Notes in Computer Science, pages 235–250. Springer, June 2012.
  * [EGM13] Javier Esparza, Pierre Ganty, and Rupak Majumdar.  Parameterized verification of asynchronous shared-memory systems.  In Proceedings of the 25th International Conference on Computer Aided Verification (CAV’13), volume 8044 of Lecture Notes in Computer Science, pages 124–140. Springer, July 2013.
  * [ES96] E. Allen Emerson and A. Prasad Sistla.  Symmetry and model checking.  Formal Methods in System Design, 9(1-2):105–131, 1996.
  * [Esp14] Javier Esparza.  Keeping a crowd safe: On the complexity of parameterized verification (invited talk).  In Proceedings of the 31st Symposium on Theoretical Aspects of Computer Science (STACS’14), volume 25 of Leibniz International Proceedings in Informatics, pages 1–10. Leibniz-Zentrum für Informatik, March 2014.
  * [GS92] Steven M. German and A. Prasad Sistla.  Reasoning about systems with many processes.  Journal of the ACM, 39(3):675–735, 1992.
  * [Kar72] Richard M. Karp.  Reducibility among combinatorial problems.  In Complexity of Computer Computations, The IBM Research Symposia Series, pages 85–103, 1972.
  * [Min67] Marvin Minsky.  Computation: Finite and Infinite Machines.  Prentice Hall International, 1967.
  * [Suz88] Ichiro Suzuki.  Proving properties of a ring of finite-state machines.  Information Processing Letters, 28(4):213–214, 1988.


# A short proof of Kneser’s Theorem via transversals

Luis Montejano

Kneser Theorem.[1] Whenever the $k$-subsets of a $n$-set are colored into
$\mathit{n-2k+1}$ colors, then two disjoint $k$-subsets end up having the same
color.

For the proof we need the following definition. A system of hyperplanes $\chi$
in $\mathbb{R}^{d}$ consists of choosing continuously one hyperplane of
$\mathbb{R}^{d}$ in every direction. That is, a system of hyperplanes in
$\mathbb{R}^{d}$ is completely determined by a function
$\varphi:\mathbb{S}^{d-1}\rightarrow\mathbb{R},$ such that for every
$x\in\mathbb{S}^{d-1},$ $\varphi(-x)=-\varphi(x).$ To see this, given
$\varphi,$ it is enough to choose, for every $x\in\mathbb{S}^{d-1},$ a
hyperplane perpendicular to $x$ through $\varphi(x)x,$ which turns out to
coincide with the hyperplane perpendicular to $-x$ through $-\varphi(-x)x,$
and vice versa. The following lemma, that follows the spirit of Dolnikov, is
crucial in the proof of the Kneser Theorem.

Lemma. Given $d$ systems of hyperplanes $\chi_{1},...,\chi_{d}$ in
$\mathbb{R}^{d}$, there is a direction in which all of them coincide.

Proof. For every $\mathbb{\chi}_{i},$ let
$\varphi_{i}:\mathbb{S}^{d-1}\rightarrow\mathbb{R}$, such that
$\varphi_{i}(-x)=-\varphi_{i}(x)$, for every $x\in\mathbb{S}^{d-1},$ its
correspondent function. Let
$\Psi:\mathbb{S}^{d-1}\rightarrow\mathbb{R}^{d-1},$ where
$\Psi(x)=(\varphi_{1}(x)-\varphi_{d}(x),...,\varphi_{d-1}(x)-\varphi_{d}(x))\in\mathbb{R}^{d-1},$
for every $x\in\mathbb{S}^{d-1}.$ Note that $\Psi(-x)=-\Psi(x).$ By the Borsuk
Ulam Theorem, there is $x_{0}\in\mathbb{S}^{d-1},$ such that
$\Psi(x_{0})=0\in\mathbb{R}^{d-1}.$ That is,
$\varphi_{i}(x_{0})=\varphi_{d}(x_{0}),$ for $i=1,...,d-1.$

Proof of the Kneser Theorem. Suppose not. Without loss of generality, we may
assume that our $n$-set is $V=\\{x_{1},...x_{n}\\}$
$\subset\mathbb{R}^{n-2k+1},$ a set of points in general position. A $k$-gone
of $V$ is the convex closure of a $k$-subset of $V$. We assume that the
$k$-gons of $V$ are colored into $n-2k+1$ colors in such a way that two
$k$-gons with the same color always intersect.

Let $L$ be a line through the origin. Choose a color, let say red. Then, the
projection of every red $k$-gone is a compact red interval contained in $L$.
Moreover, this collection of red intervals is mutually intersecting. Then, by
the Helly Theorem in the line, the intersection of all these red intervals is
again a compact interval. Take a hyperplane $H_{L},$ perpendicular to $L$,
through the middle point of the intersection of all red intervals. Clearly
$H_{L}$ varies continuously with respect to $L,$ obtaining thus a red system
of hyperplanes in $\mathbb{R}^{n-2k+1}.$ Similarly, we obtain a system of
hyperplanes for every color. By our Lemma, there is a direction in which all
these $n-2k+1$ systems of hyperplanes in $\mathbb{R}^{n-2k+1}$ coincide, but
this implies that there is a hyperplane $\Gamma$ transversal to all $k$-gons
of $V.$

To the left of $\Gamma$ in $\mathbb{R}^{n-2k+1}$, we have less than $k$ points
of $V$, otherwise $\Gamma$ would not be transversal to all $k$-gons of $V.$
Similarly, to the right of $\Gamma$ in $\mathbb{R}^{n-2k+1},$ we have less
than $k$ points of $V$, so there are $n-2k+2$ or more points of $V$ in the
hyperplane $\Gamma,$ contradicting the fact that $V\subset\mathbb{R}^{n-2k+1}$
is a set of points in general position.

## References

  * [1] Lovász, L., Kneser’s conjecture, chromatic number, and homotopy, _J. Combin. Theory, Ser. A_ 25(3) (1978), 319–324.