无线网络闲聊协议中的等式推理
Equational Reasonings in Wireless Network Gossip Protocols
AI总结:
本文提出一种基于概率定时进程演算的组合分析技术,并配备非对称模拟理论,用于证明代数定律以估计闲聊协议网络的性能,特别适用于系统非近似等价的情形。
摘要:
闲聊协议已被提出作为在大规模网络中传播信息的鲁棒且高效的方法。在本文中,我们提出了一种组合分析技术,用于研究以适用于无线传感器网络的简单概率定时进程演算表达的闲聊协议的形式化概率模型。我们为该演算配备了一种模拟理论,以比较在特定容差范围内具有相似行为的概率协议。该理论被用于证明若干代数定律,这些定律被证明在估计闲聊网络(无论有无通信冲突)以及随机化闲聊网络的性能方面非常有效。我们的模拟理论是弱互模拟度量的一个非对称变体,保留了原始定义的大部分性质。然而,我们的非对称版本特别适用于推理所考虑系统并非近似等价的情况下的协议,例如闲聊协议的情况。
英文摘要:
Gossip protocols have been proposed as a robust and efficient method for disseminating information throughout large-scale networks. In this paper, we propose a compositional analysis technique to study formal probabilistic models of gossip protocols expressed in a simple probabilistic timed process calculus for wireless sensor networks. We equip the calculus with a simulation theory to compare probabilistic protocols that have similar behaviour up to a certain tolerance. The theory is used to prove a number of algebraic laws which revealed to be very effective to estimate the performances of gossip networks, with and without communication collisions, and randomised gossip networks. Our simulation theory is an asymmetric variant of the weak bisimulation metric that maintains most of the properties of the original definition. However, our asymmetric version is particularly suitable to reason on protocols in which the systems under consideration are not approximately equivalent, as in the case of gossip protocols.
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。