Ad Hoc网络中城市街道移动模型的概率模型检测

Probabilistic Model Checking of City Street Mobility Model in Ad Hoc Network

应用概率模型检测技术,在M anhattan移动模型和街道单元移动模型的基础上,提出城市街道移动模型,将其建模成离散时间马尔可夫链DTM C s,然后运用概率模型检测工具PR ISM分析节点位置及移动情况对A d Hoc网络通信的影响。

Based on Manhattan mobility model and street unit mobility model, a city street mobility model is proposed for Ad Hoc network. A probabilistic finite state machine and Discrete Time Markov Chains （DTMCs） for this mobility model are established using probabilistic model checking. The influence of locations of nodes and mobility on the communication in Ad Hoc network is analyzed with probabilistic model checking tool-PRISM.