TY - GEN
T1 - A calculus for Mobile Ad hoc Networks from a group probabilistic perspective
AU - Liu, Si
AU - Zhao, Yongxin
AU - Zhu, Huibiao
AU - Li, Qin
PY - 2011
Y1 - 2011
N2 - Mobile Ad hoc Networks (MANETs) are networks dynamically formed by mobile nodes without the support of prior stationary infrastructures. The essential features of such a network are local broadcast, mobility and probability. In our earlier work, we proposed the p?-calculus to formally model and reason about MANTEs from a group probabilistic perspective, in which a MANET node can locally broadcast messages to a group of nodes within its physical transmission range with a certain probability. The group probabilities depend on the network topology which can evolve with the mobility of nodes. In this paper, to capture the behavior equivalence of networks, the structural congruence is investigated and the operational semantics is refined. Moreover, we define the notion of open bisimulation and prove it to be a congruence relation. Based on this, we discuss several nontrivial properties of MANETs such as mobile node equivalence and replacement. Finally, we by a case study illustrate our calculus and use it to analyze the probability of a transmission via routines.
AB - Mobile Ad hoc Networks (MANETs) are networks dynamically formed by mobile nodes without the support of prior stationary infrastructures. The essential features of such a network are local broadcast, mobility and probability. In our earlier work, we proposed the p?-calculus to formally model and reason about MANTEs from a group probabilistic perspective, in which a MANET node can locally broadcast messages to a group of nodes within its physical transmission range with a certain probability. The group probabilities depend on the network topology which can evolve with the mobility of nodes. In this paper, to capture the behavior equivalence of networks, the structural congruence is investigated and the operational semantics is refined. Moreover, we define the notion of open bisimulation and prove it to be a congruence relation. Based on this, we discuss several nontrivial properties of MANETs such as mobile node equivalence and replacement. Finally, we by a case study illustrate our calculus and use it to analyze the probability of a transmission via routines.
UR - https://www.scopus.com/pages/publications/84863039619
U2 - 10.1109/HASE.2011.13
DO - 10.1109/HASE.2011.13
M3 - 会议稿件
AN - SCOPUS:84863039619
SN - 9780769546155
T3 - Proceedings of IEEE International Symposium on High Assurance Systems Engineering
SP - 157
EP - 162
BT - Proceedings - 2011 IEEE 13th International Symposium on High-Assurance Systems Engineering, HASE 2011
T2 - 13th IEEE International Symposium on High Assurance Systems Engineering, HASE 2011
Y2 - 10 November 2011 through 12 November 2011
ER -