Home | Search | Help  
Home Page Università di Genova

Technical Report Details

Date 9-6-2010
Number DISI-TR-10-01
Title Parameterized Verification of Ad Hoc Networks
Authors Giorgio Delzanno, Arnaud Sangnier, Gianluigi Zavattaro
Bibtex Entry
E-mail giorgio@disi.unige.it
Link http://www.disi.unige.it/person/DelzannoG/Papers/dsz10.pdf
Abstract 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. We consider 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 for static, mobile, unbounded-path and bounded-path communication topology.
Back to Technical Reports