Department of Information Technology

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).

Back to the seminar page

Updated  2010-06-02 16:37:18 by Frédéric Haziza.