The Cost of Parameterized Reachability in Mobile Ad Hoc Networks

TL;DR

This paper explores the complexity of verifying reachability and other properties in automata-based models of mobile ad hoc networks, highlighting how different query types affect computational difficulty.

Contribution

It demonstrates that parameterized reachability verification is decidable with polynomial complexity and analyzes how richer queries influence this complexity.

Findings

Reachability verification is polynomial-time decidable.

Complexity increases with properties involving negation or cardinality.

The study provides insights into the computational limits of network protocol verification.

Abstract

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.