期刊名称：Electronic Proceedings in Theoretical Computer Science
电子版ISSN：2075-2180
出版年度：2011
卷号：60
页码：56-65
DOI：10.4204/EPTCS.60.4
出版社：Open Publishing Association
摘要：We summarize the main results proved in recent work on the parameterized verification of safety properties for ad hoc network protocols. We 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 we 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. The decision problem is parametric both on the size and on the form of the communication topology of the initial configurations. We draw a complete picture of the decidability and complexity boundaries of this problem according to various assumptions on the possible topologies.
