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