Specification and Verification of Position Based Routing for Mobile Ad Hoc System

This paper focus on the decidability of the position based routing in mobile ad hoc system. Based on the Abstract State Machines theory, we provide a formal model ASM PBRAgent for mobile ad hoc system, on which the position based routing runs as a query. In the result, it is shown that the problem of position based routing is PSPACE-complete when the arity of each node’s outgoing edges has a fixed upper bound, and the Yao-graph topology is an instance; on the other hand, the problem is EXPSPACE-complete if there is no fixed upper bound on the arity.