  We investigate the impact of spontaneous movement in the complexity of
verification problems for an automata-based protocol model of networks with
selective broadcast communication. We first consider reachability of an error
state and show that parameterized verification is decidable with polynomial
complexity. We then move to richer queries and show how the complexity changes
when considering properties with negation or cardinality constraints.
