Title :
Specification and Verification of Position Based Routing for Mobile Ad Hoc System
Author :
Xie, Jinkui ; Huang, Linpeng
Author_Institution :
Dept. of Comput. Sci. & Eng., Shanghai Jiao Tong Univ.
Abstract :
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
Keywords :
ad hoc networks; computability; computational complexity; finite automata; formal specification; formal verification; graph theory; mobile computing; telecommunication network routing; ASM PBRAgent; EXPSPACE-complete problem; PSPACE-complete problem; Yao-graph topology; abstract state machines theory; mobile ad hoc system; position based routing; Communication networks; Computer science; Distributed computing; Mobile ad hoc networks; Mobile computing; Network topology; Routing protocols; Self-organizing networks; Upper bound; Wireless communication;
Conference_Titel :
Computer and Information Technology, 2005. CIT 2005. The Fifth International Conference on
Conference_Location :
Shanghai
Print_ISBN :
0-7695-2432-X
DOI :
10.1109/CIT.2005.173
