Date Added: Aug 2011
The authors summarize the main results proved in recent work on the parameterized verification of safety properties for ad hoc network protocols. They consider a model in which 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 they consider a decision problem that can be expressed as the verification of the existence of an initial topology in which the execution of the protocol can lead to a configuration with at least one node in a certain state.