27 mai 2013

Arnaud Sangnier (LIAFA) salle des thèses

We study decision problems for parameterized verification of a formal model of Ad Hoc Networks with 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. We study parameterized reachability of an error state for this model and show that this problem can be solved in polynomial time. We then move to richer reachability queries with cardinality constraints and show how the complexity changes when considering different restrictions on the syntax of the queries.

This is a joint work with Giorgio Delzanno (University of Genova, Italy), Riccardo Traverso (University of Genova, Italy) and Gianluigi Zavattaro (University of Bologna, Italy).