可重构广播网络的参数化分析（长版）
Parameterized Analysis of Reconfigurable Broadcast Networks (Long Version)
摘要：
可重构广播网络（RBN）是一种分布式计算模型，其中代理可以使用某些底层通信拓扑向其他代理广播消息，这些通信拓扑可以在执行过程中任意改变。在本文中，我们进行参数化分析的RBN。我们认为立方体，（无限）集的配置在每个状态下的代理数量的上下界的形式，我们表明，我们可以评估布尔组合的立方体和可达性集的立方体在PSPACE。特别是，从一个立方体到另一个立方体的可达性是一个PSPACE完全问题。为了证明这个参数化分析的上界，我们证明了一些结构性质的可达集和符号图抽象的RBN，这可能是独立的利益。我们证明这一说法，提供这些结果的两个应用程序。首先，我们表明，几乎肯定的覆盖性问题是PSPACE完全的RBN，从而关闭从以前的文件的复杂性差距。其次，我们使用RBN定义了一个计算模型，称为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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
