一句话：给出可重构与消息丢失广播网络中覆盖性问题的 cutoff/执行长度紧界，并证明 cutoff 优化问题 NP 完全。
本文研究参数化广播网络的验证：节点相同并通过广播通信，需在任意节点数、拓扑与执行下验证性质。作者聚焦覆盖性问题，即是否存在执行到达包含指定协议状态的配置。该问题在静态网络下不可判定，在可重构网络下已知 PTIME 可判。本文给出缺失的紧界：可重构网络的最小覆盖执行长度和 cutoff 分别关于协议状态数是二次和线性。作者还引入静态拓扑但发送时非确定性丢失消息的模型，证明丢失网络有相同紧界，并指出可重构执行可比丢失执行线性更简洁。最后证明与 cutoff 相关的自然优化问题 NP 完全。
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.
@article{paperbot1328,
title = {Reconfiguration and Message Losses in Parameterized Broadcast Networks},
author = {Nathalie Bertrand and Patricia Bouyer and Anirban Majumdar},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 1},
year = {2021},
doi = {10.23638/lmcs-17(1:23)2021}
}