LSV Seminar
The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
Past Seminars
Parameterized Verification of Ad Hoc Networks
- Date
- Tuesday, October 19 2010 at 11:00AM
- Place
- Salle de Conférence (Pavillon des Jardins)
- Speaker
- Arnaud Sangnier (LIAFA, Université Paris Diderot (Paris VII))
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 a joint work with Giorgio Delzanno (University of Genova) and Gianluigi Zavattaro (University of Bologna).