移动Ad Hoc网络模拟和互模拟的进程演算

理论计算机科学电子笔记173（2007）275-293www.elsevier.com/locate/entcs移动Ad Hoc网络Massimo Merro1维罗纳大学计算机科学系意大利维罗纳摘要我们提出了一个进程演算来研究移动Ad Hoc网络的观测理论。我们的演算的操作语义是在一个减少语义和标记的过渡语义。我们证明了这两个语义一致。 标记的过渡系统，然后用来推导出的概念，adhoc网络的模拟和互模拟。 作为主要结果，我们证明了（弱）标号双相似完全刻画了（弱）约化倒钩同余，标准的、分支时间的、上下文定义的程序等价。然后，我们使用我们的（双）模拟证明方法，正式证明了一些非平凡的Ad Hoc网络的属性保留字：网络，进程演算，结构操作语义，互模拟。1介绍无线技术在过去的几年里迅速普及。它的应用范围从个人局域网、环境智能和无线局域网等用户应用到蜂窝和自组织网络等实时应用。Ad hoc网络是无线通信中的一个新领域，由于其在不需要任何固定基础设施的帮助下提供无处不在的连接的潜力而吸引了许多研究人员的注意。移动自组织网络是一个由固定和移动设备通过无线电收发器相互通信组成的自治系统移动设备可以自由地随机移动并任意地组织自己;因此，网络固定装置不能移动，即它们的物理位置不随时间变化网络可以以独立的方式操作，或者可以连接到更大的互联网。曼尼托巴坎1电子邮件：Massimo. univr.it1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.02.039276M. Merro/Electronic Notes in Theoretical Computer Science 173（2007）275l，r在有线骨干网不可行和/或经济上不方便的情况下使用，例如，在紧急情况、特殊事件（博览会、音乐会等）期间提供通信或在恶劣的环境中。无线设备使用射频信道向其他设备广播消息然而，这种形式的广播与我们在以太网网络中发现的更传统的基于有线的广播非常不同，并且从语义的角度来看，很容易理解[19，20，6]。首先，在类似以太网的系统中，广播是全球性的，即，所发送的消息到达系统的所有节点相比之下，在无线系统中，广播是本地的，即，传输跨越被称为小区的有限区域，因此仅到达系统中设备的可能为空的子集。实际上，由于环境条件（如墙壁、障碍物等），甚至小区内的设备也可能无法到达。第二，在无线系统中，信道是半双工的：在给定的信道上，设备可以发送或接收，但不能同时发送或接收。因此，两个传输之间的干扰仅可能由位于两个发射机的小区的交叉中的接收机检测到。因此，干扰是无线系统的一个微妙方面，其通过特定协议（例如，CSMA/CA）。在移动自组织网络中，还有一个问题：由于节点移动或节点移动，失败，从而改变可以接收所发送的消息的节点的集合。1.1贡献我们提出了移动Ad Hoc网络演算（CMN），一个过程演算研究移动Ad Hoc网络的观测理论。在CMN中，网络被建模为并行运行的节点（代表设备）的集合，并使用信道广播消息。通道可以是公共的，也可以是私有的，一组节点。 我们写n[P]μ为了表示具有网络地址n的节点，在物理位置l处，具有传输半径r、移动性标签μ，并且执行顺序过程P。位置l和传输半径r定义了节点可以使用信道广播值的小区;节点绝不能导出其当前物理位置l或其传输半径r。移动性标签μ用于区分移动节点和固定节点。我们假设存在适当的协议，以避免传输冲突。我们的演算的操作语义是根据归约语义和标记转换语义给出的，以Plotkin的SOS风格[18]。我们证明了这两个语义一致。我们的标签转换系统（LTS）捕捉所有可能的相互作用的一个术语与它的环境，而不使用任何辅助丢弃关系。然后，我们定义了一个适当的模拟概念，从而定义了MANN的互模拟概念模拟和互模拟的概念在文献中被广泛用于验证目的：它们是许多验证工具的基础本文的主要目标是确定两个网络何时具有相同的可观察行为，也就是说，它们在任何上下文中都是不可区分的。在本文中，我们主要关注约化倒钩同余[7]，这是Milner和M. Merro/Electronic Notes in Theoretical Computer Science 173（2007）275277名字：a，b，...，k，l，m，n，... ∈N网络：M，N：：=0空网络..M1|m2并行合成.. （ vc）M通道限制.μ工艺流程：.n[P]l，r节点（或设备）P，Q，R：：=0非活动进程..c（x）.P输入..c/w/P输出.. [w1=w2]P，Q匹配.. 一个无病毒的环境移动标签：μ：：=m移动..s平稳表1.Sangiorgi归约倒钩同余的定义简单直观。然而，在实践中，它很难用途：对所有上下文的量化是一个沉重的证明义务。更简单的证明技术是基于标记的双相似性[16，11]。作为一个主要结果，我们证明了我们的（弱）标记双相似完全特征约化倒 刺 同 余 。 然 后 ， 我 们 使 用 我 们 的 观 测 理 论 来 证 明 一 些 非 平 凡 的 属 性 的MANGORY。校样被略写或省略。在[8]中可以找到完整的证据。2微积分在表1中，我们在两级结构中定义了CMN的语法，较低的一级用于进程和网络的上层进程。我们使用字母m和n表示节点/设备;c和d表示通道;k和l表示（物理）位置;x，y，z表示变量。封闭值包含除通道和变量之外的先前值也包括变量。我们使用u和v来表示值，使用w来表示（操作）值。我们不知道怎么回事， . ，ak278M. Merro/Electronic Notes in Theoretical Computer Science 173（2007）275l，r名字。网络是节点（代表设备）的集合，并行运行符号0表示空网络。M1|M2表示两个网络的并行组成。在（vc）M中，信道c是网络M的私有信道。与其他名称传递演算（如π演算[12]）不同，限制运算符（νc）M仅对通道限制进行建模，而不是通道创建。这是因为无线系统中可用信道的数量在全世界范围内是按频率标准化的（欧洲为13个，北美为11个，日本为14个进程是连续的，并在节点中运行进程0表示非活动进程。输入进程c（x）.P可以通过通道c接收任何（闭合）值v，并继续作为P，其中v代替x。输出进程cv.P可以通过通道c发送（关闭）值v，并继续作为P。过程[v1=v2]P，Q是标准的 我们写A（x）d=e f中的一个无约束条件的定义不适用于a（p）b（x）d=ef中的定义 P，with|X轴|=|v|，其中，x表示所有字符串，并表示P中的字符串的值。每个节点具有位置和传输半径。无法创建节点或者毁灭 我们写n[P]μ对于一个名为n的节点，位于l，具有传输半径r、移动性标签μ和执行过程P。节点标识符n表示逻辑位置-设备网络地址。相比之下，l表示物理位置，并且与半径r一起用于导出关于网络连接性的信息对于移动节点，移动性标签μ可以是m，而对于固定节点，即从不改变其物理位置的节点，移动性标签μ我们并没有指出应该如何指定位置;例如，它们可以通过坐标系来给出。在操作语义的定义中，我们假设比较位置的可能性，以便确定一个节点是否位于另一个节点的传输单元内我们通过一个函数d（·，·）来实现这一点，该函数取两个位置并返回它们的距离。在第5节中，我们还假设了一些关于位置的直观元运算符在进程cw.P中，值w出现在输出位置;函数op（·）返回进程中出现在输出位置的值的集合。在过程c（x）.P中，变量x在P中是有界的，从而产生了标准的α-转换、自由变量和有界变量的概念，分别用fv（·）和bv（·）表示。类似地，在形式为（νc）M的网络中，通道名c被束缚在M中，α转换、自由通道和束缚通道的概念fc（·）和bc（·）也相应地被定义。我们写{v/x}P作为捕获，避免在P中用x代替v。我们将识别直到α转化的过程和网络。更正式地说，我们将把项看作是它们关于α的等价类的代表，并且这些代表总是被选择为使得绑定名与自由名不同。（一元）上下文C[·]是具有洞的网络项，由[·]表示。上下文由以下语法生成：C[·] ：：=[·].. [·]|M.. M|[·]..（v c）[·]。M. Merro/Electronic Notes in Theoretical Computer Science 173（2007）275279l，rdefμvμA（x）=P|X轴|为|v|impliesn[Avn]l，rn[{/x}P]l，r（StructProc）M|NN|M（结构参数通信）（M）|N）的范围|MJM|（N）|M J）（结构件装配）M|0 M（结构零杆）（vc）00（结构零分辨率）（νc）（νd）M（νd）（νc）M（结构研究）c/∈ fc（M） 蕴涵（νc）（M|N）|（vc）N（结构Res Par）[w=w]P，QP（结构然后）[w1=w2]P，Q=Q， 如果w1/=w2（其他结构）MM（结构恢复）M<$N蕴涵N<$M（结构对称）MNNO隐含MO（结构转换）MN蕴涵M|MJN|MJ，对于所有M J（结构Cxt Par）门意味 （νc）M（νc）N，对于所有c（Struct Cxt Res）表2结构一致性我们使用了一些符号约定。 网络的并行合成在限制方面优先级较低i∈IMi表示并行com-当i∈I时，所有的工作都是M i。 Wewrite（νc）Manabbreeviationforr（νc1）. （νck）M. 我们把c w写成cw。0，对于n[0]μ为0。 最后，我们写[w1=w2]P对于[w1=w2]P，0。我们假设网络中没有自由变量（相反，可以有自由通道）。随着网络的发展，自由变量的缺失被简单地维持着。此外，由于节点标识符表示设备网络地址，我们假设在任何网络中，每个节点标识符都是唯一的。2.1归约语义微积分的动力学由表3中描述的网络上的归约关系D来具体说明。与进程演算中的通常情况一样，归约语义依赖于一个辅助关系，称为结构同余，在表2中定义。基本上，结构一致性将潜在交互的参与者带入相邻的位置。规则（R-Bcast）使用信道c对消息v的广播进行建模。通信是一对多的，即使没有其他过程，传输也会继续进行280M. Merro/Electronic Notes in Theoretical Computer Science 173（2007）275li，ril，rli，rik，rl，rl，rl，rl，rl，rl，r（R-Bcast）i∈I. d（l，li）≤rn[cv.P] μ|i∈I n i[c（x i）.P i] μiDn[P] μ|i∈I ni[{v/xi}Pi]μi（R-Move）n[P]m−Dn[P]ml，r（R-Par）MDMJM|NDMJ|N（R-Struct）MNDNJ NJMJMDMJ（R-Res）MDMJ（νc）MD（νc）MJ表3归约语义侦听消息：传输是非阻塞操作。此外，与大多数进程演算一样，这种通信被认为是瞬时发生的请注意，当传输发生时，发射机范围内的某些接收机这可能是由于几个原因，例如障碍物的存在或节点的重叠。特别地，当I=0时，规则对消息丢失进行建模。就观察而言，这对应于观察者不参与的网络上的局部活动。移动被假设为一个原子动作：而移动节点不能做任何其他事情。规则（R-Move）对移动节点的任意和不可预测的移动进行建模;请注意，固定节点不能移动。其余的规则是进程演算中的标准规则。该系统不包含对数据的可靠性和可靠性的描述。2.2 行为语义学在操作语义学中，如果两个术语在所有可能的上下文中具有相同的可观察行为，则它们被认为是等价的。所以，问题是：在我们的微积分中，什么是“正确的”可观测量？在CCS [11]和π演算[12]中，我们既有消息的发送，也有消息的接收。然而，与那些演算不同的是，只能观察到消息的传输（通过不受限制的通道）事实上，在广播演算中，观察者无法看到给定的过程是否实际上接收特定广播值。特别地，如果节点n[c<$v<$.P]μ演变n[P]μ我们不能确定某个接收者在信道C接收到消息V。另一方面，如果节点n[c（x）.P]μ演化为n[{v/x}P]μ，则n可以是确保某个节点已经在信道C上发送了消息V：网络从不发明消息！因此，在我们的演算中，可观察性的概念是由可以被普适观察者检测到的消息传输来表示的，即可以在任何地方，任何通道上监听的观察者。定义2. 1WerieM↓c@kifM（νd）（n[cv. P]μ|MJ），其中ithc/∈dndd（l，k）≤r. 我们写了Mc@kifMD MJ↓c@k。在下文中，我们使用R来表示网络上的任意二元关系M. Merro/Electronic Notes in Theoretical Computer Science 173（2007）275281−−→η（输入）−CVc（x）.Pv−（输出）cv−−→−ηP{/x}PJcv.Pη−−→−PJ（然后）−−→Pη[v=v]P，Q（其他）JQ−−→Qv1/=v2ηJ−−→P{v/x}PηPJA（x）d=ef[v1=v2]P，QP−−→Q（Rec）Av−−→PJ表4标记的过渡系统-过程我们写R=来表示R的对称闭包。定义2.2关系R是倒钩保持的，如果MRN和M↓c@k意味着Nc@k.定义2.3一个关系R是归约闭的，如果MRN和MDMJ意味着N j中的一个的x是Nj的x，使得NDNJ和MJRNJ。定义2.4关系R是上下文的，如果MRN对所有上下文C[−]蕴涵C[M]RC[N]。最后，定义倒钩归约一致性的一切都已就绪定义2. 5Reductionbarbedcne3一种带标签的迁移语义在描述语言语法时，标注转换系统有两套规则：一套用于过程，一套用于网络。η表4列出了用于操作的LTS。TransitionsareoftheheformP−−→PJ，其中η的范围是输入和输出动作。 更准确地说，cv和cv表示，在通道C处分别输入和输出闭合值V。表4中的规则不言自明。λ表格5是两个工作的最终目标。Transit insareoftheheformM−−→MJ，其中λ的语法是：λ* =c？v@l..c！v[l，r]..c！v@K..τ。规则（Rcv）对在l处经由信道c接收消息v进行建模。规则（Snd）对消息v经由信道c从位于l处的节点以传输半径r的广播进行建模。规则（Bcast）对广播的传播进行建模。 要求d（l，l，J）≤r保证只有发射机的传输小区内的节点规则（Obs）模拟了每个动作c！v[l，r]可以被位于传输小区中的任何节点检测到（并因此被观察到282M. Merro/Electronic Notes in Theoretical Computer Science 173（2007）275−−→−−→≡τλ（接收）n[P]μCVP−−→−Pc？v@lJμ（Snd）CVP−−→−Pcc！v[l，r]Jcl，r −→−n[P]l，rc！v[l，r]Jc？v@lJn[P]l，r−→−J Jn[P]l，rM−→−MN−→Nd（l，l）≤r（Bcast）c！v[l，r]M|N−→−c！v[l，r]N|M−→−MJ|N JNJ|M Jc！v[l，r]M−→−MK<${k：d（l，k）≤r}K<$（观察）c！v[l，r]M−→−Mc！v@KM−→−M−（输）（移动）Jn[P]mτmM−−→Mk，r −−→n[P]l，rM−−→MJMλJ（Par）λM|NMJ|N（RES）−−→Mc/∈fc（λ）−−→λN|M−−→N|M J（νc）Mλ（νc）MJ表5标签转换系统-网络在L处，半径为R。行动C！v@K表示消息v经由信道c到一组接收者的传输，该组接收者的位置包含在K中。这是一个可观察的行为：我们可以想象一个分布式的观察者坐在K的任何位置监听通道c。规则（Lose）对消息丢失和观察者不参与的网络上的本地活动进行我们使用τ-actions来表示不可观察的动作，即观察者无法检测到的动作。规则（移动）对移动节点从位置k到新位置l的迁移进行建模。规则（Par）和（Res）是传名演算的标准规则。请注意，由于我们不传输通道，因此没有范围挤出。我们在本节结束时显示，基于LTS的语义与表3中的前一节中给出的约简语义一致。定理3.1（和谐定理）τ(i) 如果M−−→则MDM J。(ii) 如果MDMJ，则MτM.J.4双向模拟证明方法在本节中，我们使用LTS来定义adhoc网络的模拟/互模拟的适当概念。对于商品，我们使用元变量α来对那些将JJJJJM. Merro/Electronic Notes in Theoretical Computer Science 173（2007）275283−−→•c？v@l−−−−−→−−−→M，α⇒使得N==N和MRN;α用于定义（BI）模拟。从形式上讲，α：：=c？v@l..c！v@K..τ。由于我们对τ-作用上的抽象的弱行为等价感兴趣，我们引入了弱作用的概念。定义并不完全标准：·=不确定τ的真实值和初始值;==c？v@ldenotes=−→−=0;·==c！=v=@=K=表示=c！V@K1... 为c！v@Kn=0，对于nK=K;•αˆ⇒−−−−−−→α⇒−−−−−−→i=1i如果α=τand== otherwise.c！v@K注意，弱可观察行为的定义==可以包含几个（强）可观察到的行为的形式c！v @Ki. 这是因为一个分布-在几个计算步骤中在K中的每个位置处接收消息v的实例的受约束的观察者不能假设那些消息属于相同的多播发送。定义4.1网络上的二元关系R是一个模拟，如果MRN表示：• 如果MJJαjJc？v@l−→M则有NJ使得：·Nc？v@l===== NJ和MJRNJ·或N=N，N，M，R，N。我们说N模拟M，如果存在某个模拟R使得MRN。一个关系R称为互模拟，如果R和它的逆都是模拟。我们说M和N是双相似的，记为M<$N，如果存在某种互模拟R使得MRN。注意，由于消息的接收不能被直接检测到，所以消息接收的子句强加了较弱的要求，允许将输入动作与τ-动作匹配。很容易证明我们的标记双相似性是一个等价关系。然而，我们的双相似性有一个更重要的性质：上下文封闭性.引理4.2（M是上下文）设M和N是两个网络，使得M <$N。然后，(i) M|乌恩|O，对于所有网络O;(ii) （νc）M∈（νc）N，对于所有通道c。证明（草图）我们只证明了平行合成保持了π。我们• 如果Mc？v@l，则有NJ284M. Merro/Electronic Notes in Theoretical Computer Science 173（2007）275−→. . . =−→−... −−→=N⇒−−−−−−→⇒−−−−−−→−−−−−−−→ˆ⇒−−−−−→−Mτ证明关系def.ΣS= {M| O，N|O对于所有O，使得M<$N}α这是一个很好的模拟。 我们将在该试验场地M上进行试验|O −−→M.THE有趣的情况是，当过渡是由于M和O，即当使用规则（Bcast）时c！v@KL etM|O −−−−→−c！v[l，r]MbecauseM|O −−−−→−我是一个很好的朋友，d（l，k）≤r，对所有k∈K，由于应用规则（Bcast）.有两种可能：c！v[l，r]c！v[l，r]Jc？v@lJJ J• M|O −→−MbecauseMjJ−→−MandO−→O，其中d（l，l）≤rc！v@KJM=M| O.在这种情况下，通过应用规则（Obs），我们有M−−−−−−→MJ，其中KJ=K{lJ}。 当M<$N时，有NJ使得Nc！v@KJ==NJ与MjNJ. 通过向后应用规则（Obs），必须有K1，.，Kn，使得c！V@K1N=c！v@KnJnJ J−→. . .−−→=N其中i=1Ki=K且l∈Kj，对于某些1≤j≤n。 这意味着c！V@K1N=c！v[lj，rj]c！v@KnJ其中d（lj，k）≤rj，对所有k ∈Kj. 因此，通过应用规则（Bcast）：N|O =c！V@K1...为c！v[lj，rj]...c！v@Kn=NJ|OJ。最后，通过应用规则（Obs），我们可以将过渡c！v[lj，rj]−−−−−−→−c！v@Kjin−→。这意味着N|O==c！=v=@=K=NJ|OJ与.J|OJ，NJ|OJ∈S，根据需要。c！v[l，r]c？v@lJJc！v[l，r]J J• M|O−→−MbecauseM−→M和O−→−O，其中ithd（l，l）≤randM =MJ|OJ。AsMNherisNJsuchat：c？v@lJJ J J·N==N，withMN;inthisaseN|O =c！v[l，r]=NJ|OJ根据规则（Obs），也是N |O必需的.==c！=v=@=K=NJ|j，与。MJ|OJ，N J|OJ∈ S，作为·或N=N_N_J，其中M_J=N_J;在这种情况下，通过一个简单的规则（P_r），N|O =c！v[l，r]=NJ|OJand，byrulele（Obs）alsoN|c！v@KJ|OJ，与. ⇒−−−−−→−ΣMJ|OJ，N J|OJ如果需要，则∈SO==NL etM|O−−→Mc！v[l，r]becauseM|O −−−−→−M. 我们在这里住了一段时间M. Merro/Electronic Notes in Theoretical Computer Science 173（2007）275285案子剩下的情况，当M和O之间没有相互作用时，很容易处理。Q286M. Merro/Electronic Notes in Theoretical Computer Science 173（2007）275在下面的引理中，我们指出了观察谓词↓c@k和特定动作之间的密切关系引理4.3c！v@K（i）如果M−−−→− MJ则M↓c@k，对所有k∈K;(ii)如果M↓c@k，则存在值v和位置K的集合，其中k∈K，c！v@KtM−→−M.J.我们现在可以证明，我们的双相似性是一种证明方法，减少倒钩计数器，即。这是一个很好的例子。定理4.4（可靠性）设M和N是两个任意网络，使得MN，则M = N。ProofWerecallthatin=是最小的对称关系，其中hichisreduct in是封闭的、保序的和上下文的。事实上，双相似性是归约封闭的（使用定理3.1），保序的（通过引理4.3）和上下文的（通过引理4.2）。我们去吧，你去吧。Q作为主要结果，我们证明了标记双相似性不仅仅是一种证明技术。实际上，它代表了一个完整的特征化归倒钩同余。在证明完备性结果时，即约化倒钩同余包含在标记双相似性中，我们隐含地使用约化倒钩同余的标准性质。支持4. 5如果M=N，则• Mc@kiNc@k• M=MJ表示NJ满足N=Nj和MJ = NJ。引理4.6（完备性）双相似中包含约简倒刺同余。（Sketch）的Pr o f我们提供R={（M，N）|M=N}是一个简单的计算。结果将随后进行共诱导。在这个草图中，我们只考虑输出动作。c！v@K• SupposethatMRNandM−→−MJ，其中K={k1，... ，k n}。 为行动c！v@K只能由规则（Obs）的应用程序生成，它遵循c！v[l，r]thatM−→−MJ，对于任意的l和r，使得d（l，k）≤ r，对于任意的k ∈K.让我们建立一个上下文，模仿动作c的效果！v@K，以及还允许我们随后比较所考虑的两个系统的残差。我们的上下文具有以下形式：defn.ssC[·]=[·]|i=1mi[c（x）. [x=v]fi<$x<$]ki，ri|ni[fi（x）. okix]ki，riM. Merro/Electronic Notes in Theoretical Computer Science 173（2007）275287⇒S对于1≤i≤n，名称为mi，ni，对于1 ≤i≤n，通道名称为fi和oki，新鲜。直观地，在新通道fi上存在倒钩指示动作尚未发生，而在通道oki上存在倒钩连同在fi上不存在倒钩确保动作已经发生。执行。As_n=is_prereredbyne ttwork_ntext s，M_n=NimpliesC[M]_n=C[N].作为c！v[l，r]M−→−MJ，由此可见n.C[M]= MJ|i=1S基，里| n i[ok i v]Σki，ri =MwithM/fi@kianddMki，其中1≤i≤n。上述还原顺序必须与相应的还原相匹配sequenceC[N]=<$N <$ withM 当1≤i≤n时，n=N，N/fi@ki和Noki@ki。倒钩上的约束使我们能够推导出上述还原序列的结构。那就是：C[N]=N NJ|n.i=1S基，里| n i[oki⟨v⟩]s基，里N.这意味着N三！v=@=L=NJ，其中hKL。更确切地说，可以沿着同一信道执行消息V的几个输出C. 然而，由于所有节点m，i都被沿着信道c的传输到达，根据N，我们可以确定KL. 很容易证明，Nc！v@K====== NJ由在弱行动的构成中仅考虑所述产出在K中的位置，并使用规则（Lose）在τ-动作中转动其他人。ASMhave=N和约化倒钩同余通过限制保持，我们（vf，ok）M=（vf，ok）N.Aschanelsfiandoki，for1≤. i≤n，arefreshe·（vf，ok）MMJ|（vf，ok）nm[0]s|n[okv]s.i=1i基，里我我吉河·（vf，ok）N≡ NJ|（vf，ok）nm[0]s|n.[okv]s.i=1iki，riii基，里使用我们的标记双相似性和定理4.4很容易证明，.n（vf，ok）i=1S基，里| n i[oki⟨v⟩]s基，里 =0。作为一个等式，它满足Mj= NJ。Q定理4.4和引理4.6的一个简单推论如下。定理4.7（刻画）双相似性与约化倒钩同余一致。[0][0][0]=288M. Merro/Electronic Notes in Theoretical Computer Science 173（2007）275k，rl，rl，rl，rk，rl，rl，r5属性和示例在本节中，我们将使用我们的观测理论证明一些性质我们开始证明移动节点的一个有趣特性。定理5.1（移动节点的普遍性）对于任何过程P，物理位置k和l，以及传输半径r，它认为，n[P]mn[P]m.证明我们表明，关系S定义。mm=={n[P]k，r，n[P]l，r ：k，lP} I是互模拟，其中I是恒等关系。Q下一个结果表明，静默节点无法被检测到（或观察到）。如果一个节点从不发送消息，则称之为静默节点。定理5.2（静默节点不能被观察到）如果进程P不包含输出结构，那么对于任何l和r。n[P]μ0证明它来自我们对双相似性的定义，其中有可能匹配hτ-actions和带有kτ-actions的输入。我们称之为“that”=“tisthe”τreexiveanddtransitiveclosureof−−→.Q现在，我们展示了由于消息丢失，有限输出序列中的语法不同如何在语义上无法区分。定理5.3（在有限个输出序列中混合def设ALT（a，b）= c<$a<$.c<$b <$. alt.a，b. 然后，对于任何l，n，r，u和v，它成立：(i) n[ALTu，v]s(ii) n[ALT u，v]m≈n[ALTv，u]s≈ n[ALT]v，u]m 。我们只证明第二个陈述。 我们表明，关系Rd=ef. n[ALT u，v]m，n[ALT v，u]ml：对于所有k，l}=l{k，rl，r其中I是恒等关系，是一个互模拟，最大可达λ。Q这个结果可以推广到用任意有限集合替换u和v V ={v1，.，v n}的消息。更一般地说，如果两个节点只包含一个无限序列的输出结构，传输属于某个有限集合V的值，使得对于每个v∈V，输出cv出现无限次，那么这两个节点是等价的。M. Merro/Electronic Notes in Theoretical Computer Science 173（2007）275289l，rl，rl，rl，rl，rl，rl，rl，rl，rl，rl，r在下一个结果中，我们表明，传输消息的设备我们记得函数fc（·）返回一个或多个进程中包含的空闲通道的集合，而op（·）返回一个或多个进程中出现在输出位置的值的集合定理5.4（混淆消息传输）设P和Q是两个过程，使得对于某个信道c，fc（P，Q）<${c}，而对于某个信道c，op（P，Q）<${u，v}，所以我给你打电话。 LetALT（a，b）d=efca.cb. alt.a，b. 然后，(i) n[P]s(ii) n[P]m| m[ALTu，v]s| m[ALT⟨u, v⟩]m≈n[Q]s|m[ALTu，v]sn[Q]mJ|m[ALT，v]m。k，rl，rk，rlJ，r我们只证明第一个陈述。利用传递性证明了n[P]s| m[ALTu，v]s≈ m[ALTu，v]s对于所有l和r，以及对于所有P，使得fc（P）<${c}和op（P）<${u，v}。为此，我们证明了二元关系{.n[P]s| m[ALT⟨u,v⟩]s，m[ALTu，v]s：Please. fc（P）{c} op（P）{u，v}}=.sss s={n[P]l，r |m[c] v [m]。ALTu，v]l，r，m[cv. [001 pdf 1st-31files]ALT [001 pdf 1st-31files] v [001 pdf 1st-31files] l，r：P. fc（P）<${c}{P}<${u，v}}是互模拟Q这个结果也可以推广到任意有限的消息集V。下一个结果是关于范围中继器（或范围扩展器）的，并且对于固定节点（如接入点）特别有意义通常，中继器简单地重新生成网络信号，以便扩展现有网络基础设施的范围。在无线网络中，距离中继器不通过有线物理连接到网络的任何部分。相反，它从接入点、终端用户设备或另一个中继器接收无线电信号，并重新发送帧。这使得位于接入点和远处的固定用户之间的中继器可以充当在用户和接入点之间来回传播的帧的中继。以这种方式，使用距离中继器，远程用户可以在距离中继器上进行通信。可以连接到网络。在我们的计算中，一个重复可以被修改为das和nodederr[c<$→c]s得双曲余切值.进程c<$→c是一个转发进程，其一般递归定义为：a<$→ bdef=a（x）.bx这个过程在通道a接收值，并在通道b上重新发送它们;在c→c中，相同的通道c用于接收和发送。我们将在几个例子中使用转发过程290M. Merro/Electronic Notes in Theoretical Computer Science 173（2007）275k，rl，rl，rk，rSSl，r现在，假设我们想要扩展接入点n[P]s的范围. 在同等条件下-在此，假设我们想要覆盖位于l处的半径为RJ的小区。 在这种情况下，如果d（k，l）≤r且d（k，l）≤rj，则我们可以在l处添加一个距离中继器，该距离中继器简单地以传输半径RJ来回中继信号。在这种情况下，如果节点n是单信道的，即它只使用一个信道，那么距离中继器的引入允许我们模拟在l处接入点n的存在，传输半径RJ，即 n[P]sJ.定理5.5（距离转发器）设P是一个过程，使得对于某个信道c，fc（P）∈ {c}。设k，l为物理位置，r，RJ为传输半径，使得d（k，l）≤r且d（k，l）≤RJ。然后系统S.S模拟节点n[P]sJ。n[P]k，r.rr [c <$→c]l，rJ证明我们证明，关系.ss 。斯塔吉{n[P]l，rJ，n[P]k，r. rr [c <$→c]l，rJ：k，l。d（k，l）≤r <$d（k，l）≤r，p.fc（P）{c}}是一个模拟。Q然而，距离中继器的一个众所周知的缺点是，它们降低了网络的吞吐量。距离中继器必须在同一无线电频率信道上接收和转发每一帧，这实际上使发送的帧的数量加倍。特别地，相应地，对于协议CSMA/CA，每当距离中继器在信道c上发送时，节点n必须保持静默以避免冲突。避免这种不便的一种方法可以是使用在两个不同信道上工作的更复杂的测距中继器：例如，信道c用于与接入点n通信，而不同信道（比如说d）用于与本地固定用户交互。定理5.6（具有两个信道的距离转发器）设P是一个过程，使得对于某个信道c，fc（P）∈ {c}。设k，l是物理位置，r，s是传输半径，使得d（k，l）≤r且d（k，l）≤r，J。然后，对于任何通道d，系统n[P]s.. 输出[c<$→d]l，rJ.. 在[d <$→c]l中，rJ模拟节点n[{d/c}P]sJ。证明我们证明，关系.defS.S.S.sS --n[{d/c}P]l，RJ，n[P]k，r. 输出[c<$→d]l，rJ. 在[d<$→c]l中，rJ ：格但斯克湖d（k，l）≤rd（k，l）≤rJP.fc（P）}M. Merro/Electronic Notes in Theoretical Computer Science 173（2007）275291k，rl，rd（k，l）S是一个模拟。Q正如已经指出的，以前关于距离中继器的结果在处理固定节点时特别有事实上，当处理移动节点时，这些设备基本上是超级复杂的，如下所示定理5.7设k，l为物理位置，r，rJ为传输半径，r≥RJ。然后，n[P]m证明我们表明，关系模拟n[P]mJ。Sdef.mm={n[P]l，rJ，n[P]k，r：k，lP}是一个模拟。Q最后，我们提供了一个关于能源消耗的结果。众所周知[23]，位于k的节点向位于l的节点正确传输数据所需的功率p k必须满足不等式PKα ≥β，其中α≥ 2 是距离-功率梯度，β≥1是传输质量参数。2虽然β的值通常设置为1，但α的值取决于环境条件。在理想情况下，我们有α= 2;然而，在现实情况下，α通常是4。例如，对于r= 10，发射机的功率pk必须至少为10000。然而，如果我们在发送器和接收器之间引入中继器节点，比如在中间，我们可以大大降低整个传输功率。更准确地说，为了覆盖5的距离，625的发射功率就足够了。因此，发射机和中继器所需的发射功率是1250，而不是10000！下面的结果表明，在位于某个l1的第一（静止）节点和位于某个l2的第二（静止）节点之间引入中继器，使用专用信道来传播信号，不会改变原始系统的行为。注意，对于d（l1，l2）=r，我们写l1+r/2来表示位于l1和l2之间的中间位置。定理5.8（节省天线功率）设P为过程，使得fc（P）={d}，对于某个通道d。 设l1，l2为物理位置，r1，r2为传输半径，使得d（l1，l2）= r，r≤r1，且r ≤r2。然后系统.S.S.s（vd） m[P]l1，r/2.rr [d <$→ d]l1+r/2，r/2.n[Q]l2，r2模拟系统.（vd）Sl1，r1.Σ.n[Q]l2，r2.2该不等式适用于视线无障碍的自由空间环境，并且没有考虑可能发生的反射、散射和由建筑物、地形等引起的方向性。然而，它在adhoc网络社区中被广泛接受。m[P]292M. Merro/Electronic Notes in Theoretical Computer Science 173（2007）275l，r11Sl、r/21SS证明这两个系统基本上是不同的距离中继器op-erating在私人通道d的存在。形式上，我们证明，关系.{（νd）（m[P]s..n[Q]l2，r2），（νd）（m[P]s.. rr [d <$→ d]l1+r/2，r/2.Σ. n[Q]l2，r2）：fc（P）={d}}是一个模拟。Q6相关和未来的工作Prasad [19，20，15]在他的《广播系统微积分》（Calculus of BroadcastingSystems，CBS）中首次分析了类似以太网通信的广播，其中所有进程都同时接收广播消息。在[21]中，同一作者提出了一个LTS和一个（强和弱）标记的双相似性依赖于“丢弃关系”的概念，这是一个特殊的过渡，任何过程都可以执行以丢弃潜在的消息。从技术上讲，丢弃关系是一种将广播的语义与并行组合的语义相匹配的机制。Hennessy和Rathke [6]证明了上述（弱）双相似性，重新命名为噪