https://bans.imag.fr/b/rad-ofn-9t8-rqc
5 May 2022 - 10h00
Reconfigurable Parameterized Broadcast Networks: Minimal Size and Execution Length for Coverability
by Nathalie Bertrand from INRIA Rennes
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 work we establish 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. Joint work with Patricia Bouyer and Anirban Majumdar
This is a MOHYTOS seminar.
