摘要：Broadcast networks allow one to model networks of identical nodescommunicating through message broadcasts. Their parameterized verification aimsat proving a property holds for any number of nodes, under any communicationtopology, and on all possible executions. We focus on the coverability problemwhich dually asks whether there exists an execution that visits a configurationexhibiting some given state of the broadcast protocol. Coverability is known tobe undecidable for static networks, i.e. when the number of nodes andcommunication topology is fixed along executions. In contrast, it is decidablein PTIME when the communication topology may change arbitrarily alongexecutions, that is for reconfigurable networks. Surprisingly, no lower norupper bounds on the minimal number of nodes, or the minimal length of coveringexecution in reconfigurable networks, appear in the literature. In this paper we show tight bounds for cutoff and length, which happen to belinear and quadratic, respectively, in the number of states of the protocol. Wealso introduce an intermediary model with static communication topology andnon-deterministic message losses upon sending. We show that the same tightbounds apply to lossy networks, although, reconfigurable executions may belinearly more succinct than lossy executions. Finally, we show NP-completenessfor the natural optimisation problem associated with the cutoff.
