Parameterized Verification of Safety Properties in Ad Hoc Network Protocols
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.