Paper Info
Title
Verification of Directed Acyclic Ad Hoc Networks.
Abstract
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.
Year
DOI
Venue
2013
10.1007/978-3-642-38592-6_14
Lecture Notes in Computer Science
Keywords
Field
DocType
computer science
Parameterized complexity,Decision problem,Vertex (geometry),Computer science,Directed acyclic graph,Theoretical computer science,Decidability,Reachability,Wireless ad hoc network,Bounded function
Conference
Volume
ISSN
Citations 
7892
0302-9743
6
PageRank 
References 
Authors
0.44
12
3
Name
Order
Citations
PageRank
Parosh Aziz Abdulla12010122.22
Mohamed Faouzi Atig250540.94
Othmane Rezine3263.80