Parameterized Verification of Ad Hoc Networks

Speaker

Arnaud Sangnier (Paris 7)
Title Parameterized Verification of Ad Hoc Networks
When 11.05.2011, 11:00
Where Seminarraum Informatik 7
Abstract We study decision problems for parameterized verification of a formal model of Ad Hoc Networks with selective broadcast. 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 are interested in decision problems that are parametric on the size and on the shape of the communication topology of the initial configurations. We draw a complete picture of the decidability boundaries of these problems according to different assumptions on the mobility of the nodes in the networks and on the form of the communication graphs.

This is a joint work with Giorgio Delzanno (University of Genova) and Gianluigi Zavattaro (University of Bologna).
Slides