参数化广播网络中的重新配置和消息丢失
摘要：广播网络允许建模具有相同节点的网络，通过信息广播进行通信。它们的参数化验证旨在证明对于任意数量的节点，在任何通信拓扑和所有可能的执行中，某个属性都成立。我们关注的是覆盖性问题，双重地询问是否存在一种执行方式，该执行方式访问到广播协议中展示某个给定状态的配置。已知静态网络的覆盖性是不可判定的，即当节点数量和通信拓扑固定在执行过程中。相反，当通信拓扑可以在执行过程中任意改变时，即对于可重新配置的网络，覆盖性在PTIME下是可判定的。令人惊讶的是，关于可重新配置网络中节点的最小数量或最小覆盖执行长度的下界和上界在文献中都没有出现。 在本文中，我们展示了截断和长度的严格界限，它们分别与协议状态的数量呈线性和二次关系。我们还引入了一个具有静态通信拓扑和发送过程中的非确定性消息丢失的中间模型。我们证明了相同的严格界限适用于有丢失的网络，尽管可重新配置的执行可能比有丢失的执行更加简洁。最后，我们证明了与截断相关的自然优化问题是NP完全的。
作者：Nathalie Bertrand and Patricia Bouyer and Anirban Majumdar
论文ID：1912.07042
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22