论文标题
可重构广播网络的参数化分析（长版）
Parameterized Analysis of Reconfigurable Broadcast Networks (Long Version)
论文作者
论文摘要
可重新配置的广播网络（RBN）是分布式计算的模型，在该模型中，代理可以使用一些基本通信拓扑传播给其他代理，这些拓扑可以在执行过程中任意改变。在本文中，我们对RBN进行参数化分析。我们考虑了每个状态中代理数量的下部和上限形式的立方体（无限）配置集，并且我们表明我们可以评估Pspace中立方体和可及的立方体的布尔组合。特别是，从立方体到另一个立方体的可及性是PSPACE完整问题。 为了证明该参数化分析的上限，我们证明了有关RBN的可及性集和符号图抽象的一些结构属性，这可能具有独立的关注。我们通过提供这些结果的两个申请来证明这一主张是合理的。首先，我们表明，几乎纯净的覆盖性问题对于RBN来说是PSPACE的完整问题，从而缩小了先前论文的复杂性差距。其次，我们使用rbn，àla总体协议（称为RBN协议）定义一个计算模型。我们精确表征了可以通过此类协议计算的一组谓词。
Reconfigurable broadcast networks (RBN) are a model of distributed computation in which agents can broadcast messages to other agents using some underlying communication topology which can change arbitrarily over the course of executions. In this paper, we conduct parameterized analysis of RBN. We consider cubes,(infinite) sets of configurations in the form of lower and upper bounds on the number of agents in each state, and we show that we can evaluate boolean combinations over cubes and reachability sets of cubes in PSPACE. In particular, reachability from a cube to another cube is a PSPACE-complete problem. To prove the upper bound for this parameterized analysis, we prove some structural properties about the reachability sets and the symbolic graph abstraction of RBN, which might be of independent interest. We justify this claim by providing two applications of these results. First, we show that the almost-sure coverability problem is PSPACE-complete for RBN, thereby closing a complexity gap from a previous paper. Second, we define a computation model using RBN, à la population protocols, called RBN protocols. We characterize precisely the set of predicates that can be computed by such protocols.
