Verification of Directed Acyclic Ad Hoc Networks
Verification of Directed Acyclic Ad Hoc Networks
复制标题
有向非循环自组织网络的验证
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Othmane Rezine
中科院分区：
文献类型：
--
作者：
P. Abdulla;M. Atig;Othmane Rezine
研究了自组织网络形式化模型的参数化验证决策问题。我们考虑一个模型，其中网络是由一组通过有向无环图相互连接的过程组成的。图中的顶点表示各个过程的状态。相邻顶点表示单跳邻居。进程是具有本地和同步广播转换的有限状态机。广播的接收仅限于发送方进程的近邻。底层连接图将通信模式限制为仅一个方向。这允许建模典型的通信模式，其中数据从一组中心节点传播到网络的其余部分，或者从另一个方向收集。对于该模型，我们考虑控制状态可达性（可覆盖性）问题的可判定性，该问题定义在两类体系结构上，即所有无环网络的类（我们显示不可判定性）和具有有限深度的无环网络的类（我们显示可判定性）。决策问题由基础网络的大小和拓扑结构参数化。
We study decision problems for parameterized verification of a formal model of ad hoc networks. We consider a model in which the network is composed of a set of processes connected to each other through a directed acyclic graph. Vertices of the graph represent states of individual processes. Adjacent vertices represent single-hop neighbors. The processes are finite-state machines with local and synchronized broadcast transitions. Reception of a broadcast is restricted to the immediate neighbors of the sender process. The underlying connectivity graph constrains communication pattern to only one direction. This allows to model typical communication patterns where data is propagated from a set of central nodes to the rest of the network, or alternatively collected in the other direction. For this model, we consider decidability of the control state reachability (coverability) problem, defined over two classes of architectures, namely the class of all acyclic networks (for which we show undecidability) and that of acyclic networks with a bounded depth (for which we show decidability). The decision problems are parameterized both by the size and by the topology of the underlying network.