Parameterized Verification of Ad Hoc Networks

We study decision problems for parameterized verification of a formal model of Ad Hoc Networks with selective broadcast and spontaneous movement. The communication topology of a network is represented as a graph. Nodes represent states of individual processes. Adjacent nodes represent single-hop neighbors. Processes are finite state automata that communicate via selective broadcast messages. Reception of a broadcast is restricted to single-hop neighbors. For this model we consider verification problems that can be expressed as reachability of configurations with one node (resp. all nodes) in a certain state from an initial configuration with an arbitrary number of nodes and unknown topology. We draw a complete picture of the decidability boundaries of these problems according to different assumptions on communication graphs, namely static, mobile, and bounded path topology.

• Type: Conference
• Year: 2010
• Where: CONCUR
• Authors: Giorgio Delzanno, Arnaud Sangnier, Gianluigi Zavattaro
• Keywords: CONCUR 2010, Distributed And Parallel Computing, Nodes Represent States, Selective Broadcast, Single-hop Neighbors