Parameterized Verification of Ad Hoc Networks
Arnaud Sangnier, Università di Genova, Italy
- Date and Time
Thursday, June 10th, 2010 at 13:30
Polacksbaken, room 1145
We study decision problems for parameterized verification of a formal model of Ad Hoc Networks with selective broadcast and spontaneous movement recently proposed by Singh, Ramakrishnan, and Smolka.
The communication topology of a network is represented here 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. All decision problems are parametric both on the size and on the form of the communication topology of the initial configurations. We draw a complete picture of the decidability boundaries of these problems according to various assumptions on the communication topology of the network, namely static vs mobile and unbounded- vs bounded-path topologies.
This is a joint work with Giorgio Delzanno (University of Genova) and Gianluigi Zavattaro (University of Bologna).