  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.

Logic in Computer Science