带寄存器的参数化广播网络：从NP到可判定性边界

我们考虑任意大规模智能体网络的参数化验证，这些智能体通过广播和接收消息进行通信。在我们的模型中，广播拓扑可重新配置，使得发送的消息可被任意智能体集合接收。此外，智能体具有初始互异的本地寄存器，因此可视为标识符。当智能体广播消息时，它将一个寄存器中存储的值附加到消息上。接收时，智能体可存储收到的值或将该值与自身某个寄存器进行相等性测试。我们考虑覆盖问题，即询问系统给定状态是否至少可被一个智能体到达。我们确立该问题可判定；然而，其难度等同于丢失信道系统中的覆盖问题，而后者是非原始递归的。该模型位于可判定性边界，因为此模型上的其他经典问题不可判定；特别是要求所有进程同步于给定状态的目标问题即如此。相比之下，我们证明当每个智能体仅有一个寄存器时，覆盖问题是NP完全的。