泰山：无线网络图重写框架对物理变量的表示和正式语义

理论计算机科学电子笔记112（2005）77-94www.elsevier.com/locate/entcs泰山：在无线丛林埃米利奥·托斯托Dipartimento di Informatica，Via F.Buonarroti 2，56127比萨摘要无线网络允许便携式/移动设备（和相关应用）利用无线电或红外信号彼此通信。在这些网络上的计算对许多物理变量（例如，能耗、距离、地理拓扑等）。我们提出了泰山，一个框架的基础上图重写，很容易让一个无线网络的许多定量方面表示。除了表现力的问题，泰山的主要优势是其正式的语义，可以利用指定的应用程序，路由算法或协调方面的无线设备考虑现实的物理限制。保留字：无线网路，图改写，边置换，同步。1介绍无线设备的网络呈现出在有线网络中不重要或不重要的特性。其中，网络拓扑结构的动态性无线网络的拓扑是高度动态的，因为节点通常是便携式计算设备（例如，移动电话、PDA、膝上型计算机等）。由于电池消耗，节点可以异步消失。除了对设备之间的交互和拓扑的动态性的影响之外，这也是一个重要的问题，因为无线网络通常是对等网络，其中任何节点都可以充当网关。无线设备具有有限的*这项工作得到了欧洲EU-FET项目PROFUNDIS IST-2001-33100和MIUR项目SP4“ A rc h i t e tt u r e S of t w a r e ad Al t a Q u a l i t ` a d i S e r v iz i o pe r Gl o b a l Co m pu t i n g su Co o pe r a t i v e Wi d e Ar e a Ne t w o r k s ”的 支持 。1571-0661 © 2004由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2004.01.02278E. Tuosto/Electronic Notes in Theoretical Computer Science 112（2005）77传输能力。因此，通信并不总是得到保证;此外，外部环境可能会引起干扰或阻断通信。总之，无线网络提出了许多问题，这些问题本质上涉及计算中必须考虑的几个定量方面。一般来说，这些方面被单独考虑，并在数学设置中进行研究，该数学设置对设备的物理特性和外部环境的路由算法进行建模。据我们所知，目前还缺乏一个正式的框架来表达上述讨论的现象在一个基于图的技术可以被用于建模互联网络系统。实际上，边可以用于表示系统的组件，而节点对组件的同步端口进行建模。共享一个节点的两个（或多个）边表示在通信端口上连接的组件;相邻的边可以同步。图可以通过操作语义学的方式被适时地同步。基于边替换和同步的图重写在[2，5]中被引入，并且在[14]中与分布约束满足问题相关。最近在[9，10，6，16]中考虑了移动性，其中研究了同步超边缘置换我们认为纯粹的局部图同步结合图重写和约束求解。直观的想法是，局部重写依赖于约束满足算法的结果。我们的框架是对[6]中SHR方法的简化，并允许相互关联修改。节点可以在同步过程中交换这相当于组件的移动性，可以动态地改变它们的连接。在SHR方法的顶部，我们描述了泰山，一个语义模型，适合处理这些方面的无线网络。有趣的是，图重写似乎适合描述一些传统分布式计算模型显然无法捕捉的现象（至少以简单的方式，参见第2节和第6节的讨论）。特别是，通信干扰可以简单地表示在一个正式的方式占正式推理的无线网络。这似乎是一个有趣的和未完全探索的领域;事实上，引用[7]：对于共享相同频谱的ad-hoc网络，需要新的合作方法来实现共存。这些方法很难在没有真实信道模型和仿真方法的情况下进行研究;在这一领域仍然有基础工作要做[13]。除了理论上的兴趣，我们建议泰山作为一种正式的语言E. Tuosto/Electronic Notes in Theoretical Computer Science 112（2005）7779|||||用于表达无线网络中的计算并对物理环境进行建模。正如稍后将更清楚（第5节）的环境类似于一个茂密的植被与藤本植物的热带丛林，泰山（无线设备）摆动和叫喊寻找简（他的合作伙伴）。即使我们不解决无线协议设计，这种方法也可以帮助设计人员正确指定他们的协议。论文的结构。第2节简要讨论了传统的分布式计算模型在考虑无线通信时所面临的困难第3节给出了对SHR的直观解释。第4节报告了超图和乘积的形式定义;此外，在第4.3节中通过一个例子给出了SHR的直观操作解释。为了使表述尽可能简单，我们将SHR的正式定义放在附录A中。泰山的制作在第5节中定义。最后评论见第6节。2无线网络和传统模式与有线网络不同，无线设备可以在没有预先存在的通信基础设施的情况下彼此交互实际上，它们通常配备有无线电和红外发射器/接收器。在无线系统上建模和推理的语义框架本质上比“有线系统”的框架更难定义主要原因是通信基础设施不允许通过名称来个性化组件的位置（如第1节所述）。这不仅对于组件的交互建模是有问题的，而且还因为语义模型应该包含距离的概念。事实上，该框架应该对拓扑（连同其几何/物理结构）、网络结构和两个组件之间的距离、它们的传输容量等进行建模。像Ambient [1]或KLAIM[4]这样的传统框架似乎无法以优雅的方式捕捉这些 方 面 的 大 部 分 。环 境 系 统 是 环 境 的 平 行 组 成 ， 并 且 是 f 的 项 [P1..Pnb1[. . . ]。 .bm[. . . ]]（a，bi因此，如果一个环境系统的拓扑结构是一个森林的树木。进程“在空中”发送消息，接收它们并通过系统拓扑引导其周围环境。 消息的条件是接收到的是消息和接收者必须在相同的环境中。然而，该“邻近”条件不包含任何距离概念，因为并行合成运算符|是可交换的，因此80E. Tuosto/Electronic Notes in Theoretical Computer Science 112（2005）77−→−→a [P|Q|R]等于[P|R|Q]。在K LAIM系统中，是节点s：：P1的并行组合|......这是什么？|P n, where s is the name of the node, P i’s are either processes running at sor tuple of data allocated at s.进程可以生成元组，通过模式匹配输入元组，并在节点间漫游。KLAIM消息在最近，K LAIM已经配备了语言机制来控制节点之间的链接[3]。链接的创建和删除可以编程，该语言还可以表达依赖于应用程序的链接功能。事实上，节点之间的距离可以很容易地在这种情况下表示。然而，Ambient和KLAIM都不能容易地对无线通信的有趣现象进行建模，即由第三方移动引起的对通信的干扰。实际上，两个无线设备D1和D2之间的通信可能被移动通过分隔它们的空间的另一个组件（不一定是设备）干扰这种现象在传统框架中难以捕捉，因为即使链路包含节点之间的距离，它也在连接的节点和第三实体不能3超图：概述图文法[15]是作为字符串文法的扩展而提出的。类似于字符串的文法，图文法的产生式具有形式L其中L和R是图，并指定图如何 被重写。L R上的条件允许引入“上下文无关性”的概念超图是由节点和超边组成的图，超边是边的推广;超边可以被认为是连接两个以上节点的边。 传统图中的边可以直观地认为表示两个节点之间的二元关系，而超边表示许多节点之间的关系。我们将描述一种基于同步超边替换的重写机制图1旨在给出超边缘替换的直观性。图1（a）中的超边L通过其外部节点（或附着点）1，. 图1（b）表示用超图G代替L得到的超图。图1（b）的虚线灰色部分表示初始情况，并且在L已经被确定之后消失E. Tuosto/Electronic Notes in Theoretical Computer Science 112（2005）7781∈ L(a)一个超边L（b）用G代替LFig. 1.超边缘替换替换为G;请注意，重写中不涉及G1而且，新的节点可以出现（G中除了1和2之外的所有节点都是由过渡产生的新节点），并且一些节点可以在过渡之后被节点4与5融合）。正如稍后将显示的，这相当于组件的移动性，可以动态地改变它们的连接。事实上，请注意，在图1（b）中，连接到节点4的G2部分对应于图1（a）中连接到节点5的G2J部分。4超图下面我们考虑固定的一组节点N和一组按自然数排序的标签L;L：n表示标签L∈L，秩为n。超图是由超边和节点构成的。标记为L的超边（或简单的边）可以连接与其秩一样多的节点 我们写L（x1，.， xn）以指示连接到附接节点的标记为L的边x1，.，xn. 例如，图1（a）中的超边L被写为L（1，.，5）。从节点1，.，5至L是L的连接点，称为触手形式上，超图是句法判断：定义4.1ΓG是一个句法判断i• N是节点的有限集合，• G是由以下语法G：：= nil_L（x1，. ..，xn）|G，其中x1，.，xn是节点并且L使得L：n。 我们称项G设n（G）表示出现在G中的节点的集合。定义4.1中的产生式允许生成空图（由nil表示）、单边（使用L（x1，.，xn））和构成项，82E. Tuosto/Electronic Notes in Theoretical Computer Science 112（2005）77·→∈并行（通过G|G）。在下文中，我们使用“graph”作为“hyper- graph”的同义词，并在写x1，...，x nG而不是{x1，.，x n}{\displaystyle x n }{\displaystyle x n}{\displaystyle x n}4.1超图同步SHR是通过图重写和约束求解相结合得到的。更具体地说，我们使用与上下文无关的制作，并标记有可用于协调制作的同时应用的动作协调重写允许在应用产生式的整个图上传播同步确定在给定阶段同步的生产对应于解决分布式约束满足问题[14]。SHR方法的主要特征是，当超边施加在其外部节点上的条件与相邻超边施加的条件以及所采用的同步策略一致时，超边可以被替换可以生成新的节点，交换节点和融合它们。观察4.1每个边重写必须与一个或多个相邻边同步。取决于所选择的同步算法，边缘的数量可以变化。本文主要研究了同步化机制，（CSP[11]，其中S（a，a）=a）和a′l a Milner（CCS[12]，其中S（a，a′）=τ）同步化[17]（传统上，可以认为a ′是输出动作，而a表示输入动作）。前者要求同步的所有参与者执行相同的动作，而后者则需要两个参与者通过互补的动作来同步。此后，我们认为同步化是一个米尔纳。在下文中，我们假设固定的Cons，这是一组用于命名超边外部节点上约束图重写的条件的动作。由于我们使用Milner同步，Cons还有两个进一步的成分：• 一个互补运算<$：Cons Cons使得对于任何aCons，a<$=a;• 一种表示同步的独特的无声动作τ此外，我们假设任何标签a∈ 缺点有一个arity;我们让|· |：Cons→ωe是Cons上的arry y函数，对于a∈Con s，|一|=的|a'|.E. Tuosto/Electronic Notes in Theoretical Computer Science 112（2005）7783→N {} ∈ L−−→π联系我们↑| |∈4.2Productions一个图重写系统G=<$Γ0<$G0，P <$由一个初始图Γ0<$G0和一组产生式组成.在定义生产之前，我们需要一个辅助定义。定义4.2[融合替换]设X是一组节点。X上的融合取代是函数π：X→X，使得<$x，y∈X.π（x）= y <$π（y）= y.一个融合置换π：X X诱导了一个等价关系π在defx定义为xπ 关于我们 π（x）=π（y）。 等价π 将X划分为等价类，并且每个节点x∈X被映射到其类的代表元素π（x），即唯一元素y，使得π（y）=y。定义4.3[生产]设X是集合x1，.，xn和L使L：n。一部作品是一种形式的过渡XL（x1，.，xn）Λ>ΓG，（1）其中n（G）≠Γ，- Λ<$X × Cons ×N <$<$是一组约束，它们是三元组（x，a，y），使得y的长度为a。给定Λ，我们说y是约束（x，a，y）Λ的节点，并且Λ（x）表示（a，y），而Λ（x）表示Λ不对x施加约束（即（xJ，a，y）Λ意味着x=xJ）。我们让n（Λ）表示Λ中约束的节点- π：X→X是融合替换，使得n（Λ）<$X<$π（X）（即，用于同步的外部节点必须是根据π的代表元素）;- r =π（X）<$（n（Λ）\X）。节点x1，.，xn是L到周围环境的附着节点，即L可以与其他边共享它们。产品指定环境必须满足的约束，以便替换边。这样的约束由Λ施加在L的外部节点的集合X上;动作的arities必须等于约束的节点数。A将节点的动作和序列关联到（一些）外部节点，L.直观地说，与连接节点相关联的动作约束了图的可能重写;实际上，只有当外部节点上的动作根据所采用的同步策略与相邻边的产生所施加的动作同步时，才能应用产生式（1如果84E. Tuosto/Electronic Notes in Theoretical Computer Science 112（2005）77EE∈u1n（x，a，y）Λ，则L可以与环境中具有连接到x的条件并满足条件a的边同步。现在让我们考虑生产（1）的右边的结构。Γ由x 1的镜像节点组成，. ..一般来说，G可以是任何图（只要n（G）≥r）。在该followingg中，我们写入X_L（x， . . ， x）−−Λ→>Γ<$G，对于一个乘积其融合替换是恒等函数。一旦满足Λ中的约束，节点必须根据融合替换π合并。4.3同步生产本节提供了SHR的应用示例我们更喜欢尽可能简单地离开正式机制见附录A。我们不使用对产品的“文本”描述，而是直接用图表来描述它们。以下结果表示边可以如何迁移。我们将在泰山框架的设计中利用它们。我们考虑一个简单的例子，其中两条边E：3和D：1相互作用。生产¯l⟨z⟩E·=··x·yxyz z说明边E（x，y，z）在节点x上与l-动作同步，并与其第三个节点z通信。在同步之后，E保持不变。第二次生产的E-边缘是·El·u=···xyxyz·auz·并且声明E（x，y，z）分别在节点y和z上同时与动作l和a同步。在生产的rhs中，出现了新节点u。直觉是，来自相邻E-边缘的节点以l同步被接收，并且被传送到连接到z的边缘。EdgeD只有一个生产zJDa·w=公司简介•·DE. Tuosto/Electronic Notes in Theoretical Computer Science 112（2005）7785x·E·yE·x·ED·z·yw=u（一）E··zJz·（b）第（1）款图二. 边缘移动说明当D（ZJ）在ZJ上与动作a同步时，则接收到新节点w;在同步之后，连接到ZJ的D-边被取消，并且D-边的新实例出现在新节点w上。让我们考虑下图（触角已经用产品的动作进行了注释）：x·awE阿库乌河·z洛乌河 ·y¯l⟨zJ⟩·z·J（二）图（2）的重写由以下步骤确定：(i) 个别化的相邻触角标记的互补行动;(ii) 确定同步生产;(iii) 用相应的RHS替换出现在同步产品的LH中的边缘（的实例）;(iv) 融合那些被同步等同的节点。让我们将前面的模式应用于图（2）。步骤（i）已经在（2）中完成;步骤（ii）很容易：E-边的最右边和最左边的实例分别被E-边的第一和第二产生式重写，而对于边D只有一个可能的产生式。步骤（iii）产生图2（a）中的曲线图。由于同步施加等式w=u=zJ，步骤（iv）简单地融合w和zJ，确定图2（b）中的图，其中D从z移动到zJ。本节中对SHR的直观描述建议采用以下设计风格：• 将系统表示为多个组件;• 对于每个组件，绘制一个超边，以便解释其外部节点（如所报告的示例）;• 然后，在外部节点上，写入将约束超边缘重写的动作;• 最后，指定将用超边替换的图EzJ··DD86E. Tuosto/Electronic Notes in Theoretical Computer Science 112（2005）77Ex1x2···z(a) 环境边缘(b) 环境图图三. 环境边和图注意图的外部节点满足定义4.3的条件。下面我们就采用这种设计风格。5泰山我们利用前面几节中报告的图形演算来对无线设备及其运行的“环境”进行建模。我们的框架，泰山，利用SHR的声明性的声明，因为设备是自主的，而移动性是通过节点融合实现的。 我们不考虑所有的问题之前讨论过，但给他们如何可以在泰山建模提示。通过连接具有三个触角的环境边E：3来构建环境，并且可以如图3（a）所示。 边E（x1，x2，z）可以被认为是组成理想“以太”的原子项如图3（b）所示，我们可以把环境想象成热带丛林中的一个繁茂植被，有很多藤本植物，泰山（一个无线设备）在那里摇摆，大声寻找简（他的伴侣）。信号传播，无线设备和环境边缘的产品如下。信号制作我们要建模的信号的主要特征是：（i）频带频率，（ii）强度和（iii）方向。通常，应考虑其他信息，例如，信号携带用于路由或应用的然而，我们只想定义一个框架来描述信号如何在给定环境中传播。考虑更多的信息边缘是一个简单的通则，E. Tuosto/Electronic Notes in Theoretical Computer Science 112（2005）7787Ry·Rr+1B0定义如下：1。我们假设存在由Sf，d标记的元1的信号边缘，其中 f是频带频率，d是方向（稍后说明），r是抽象信号强度的自然数。信号边缘的产生非常简单：只要强度不为空，信号就试图沿着指定的方向传播：W. . . . ·f，d w，z=.f，dry•z.只有非零强度的信号才能传播。直觉是，Sf，d从环境中获取节点w和节点z，其中节点w是沿着方向d的下一个节点，节点z可能连接有设备。在同步之后，较弱的信号边缘Sf，d被附加到w，并且信息边缘S考虑与在该方向上（可能）遇到的设备的交互。S-边的产生式是：Sm<$ ···=·和τ·=·z z z z第一个产生式考虑的是信息到达连接到z的设备的情况，而第二个产生式则表示消息可以在没有被接收到的情况下消失。这模拟了没有设备连接到z的情况。动作m通常取决于必须被执行的消息变了在这里，我们不考虑相关的信息，因为它们取决于我们想要描述的应用程序。设备生产与信号边沿类似，器件边沿的arity为1。我们感兴趣的器件的主要特征是：（i）能级，和（ii）传输能力。我们认为恒定的传输功率的去-反之亦然，而能量水平被处理为信号边缘的强度。设备边缘由Dr标记;r是设备的载波感测半径，并且b表示D的剩余能量（为简单起见，我们可以假设b是正整数）。[1]这里我们不考虑广播信号，这些信号可以以米尔纳同步的一些复杂性为代价进行建模，而霍尔同步可能更适合。2如果我们想收集垃圾信号，可以为S f，d指定类似的产生式。3情况并非总是如此，但我们希望尽可能简单地进行演示我们产品的简单变化可以很容易地处理一般情况。Sf，dr+1SSS.·88E. Tuosto/Electronic Notes in Theoretical Computer Science 112（2005）77DrBτ⟨⟩·DrB'Sf，dRbE·E····BB≤Rb0B我们首先考虑处理能源消耗的生产=bJb（3）z zrτ=zb> 0。（四）z生产（3）指出，设备的能量水平可以非确定性地降低。条件bJ=b捕获D表示插入设备的情况。初看起来，产生式（4）可能显得很奇怪;它表明，一个放电的装置突然获得了一些能量。基本上，这模拟了设备在给定时间打开器件移动性的建模类似于信号的传播：rmvdzJ=zz•bJ≤b;zJDr询问注意，在这种情况下，能量水平也可能降低。最后一个生产处理信号的发射：rem f，dbz·Z x•·BJΓ2πG2（A.1）其中Λ，π，Γ2和G2服从与产生式相同的条件。本质上，变迁可以被看作是在其lhs上具有一般图的产生式因此，变迁描述了图的动态演化转换（A.1）表示根据约束Λ重写，并确定融合替换π。生产是同步通过表A.1中的推理规则。我们称idle为一个具有空条件集的产生式，而恒等函数为融合置换。定义A.1[图的变迁]设Γ0G0，是一个图的重写系统。 转换集T（）是包含任何闲置生产，并根据表A.1中的推理规则关闭。通过从初始图开始并通过执行一系列转换来获得派生，每个转换通过同步产生来重写规则的同步需要动作的匹配和约束Λ的第三分量的统一。在应用产生式之后，统一函数用于通过合并相应的节点来获得最终图。在表A.1中，我们使用符号[v1，...，vn/u1，.，un]（缩写为[v/u]）来表示应用于图和约 束 集的替换。E. Tuosto/Electronic Notes in Theoretical Computer Science 112（2005）7793Γ， y<$G−−π→> ΓJ<$GJΛ（合并1）Γ<$[x/y]G−→>n（ρΛ）<$（π;ρ）−y（Γ）<$ρGJΛ（y）↑xπyy/=π（y）ρ=[π（x）/π（y）]ρΛ（π;ρ）−yΓ，y►G−→Λ<${（x，a，v），（y，a，w）}π联系我们JGJ（合并2）[x/y]wXy=π（y）ρ=mgu{[/π[x/y]v]，[π（x）/π（y）]}的情况ΓJJ = n（ρΛ）<$（π;ρ）−y（Γ）U=ρ（ΓJ）\ΓJJ[ /]G−−→Xy（ρΛ（x，τ，τ））JJJ（π;ρ）−y>τν U.ρGΓ1<$G1−−π→> Γ2<$G2ΛΓJ1<$GJ1−−π→J> ΓJ2<$GJ2ΛJ（面值）（Γ1<$ Γ2）<$（ΓJ1<$ΓJ2）=<$Γ∪Γ►G|G−→>ΓΓG|G1111Λ∪ ΛJ22π∪πJ22表A.1图同步若ρ = [v/u]是一个置换，则ρG是对任意i = 1，. n，而ρ Λ ={（x，a，ρy）：（x，a，y）∈ Λ}其中ρy是序列ρ（y1），.，ρ（yh），如果y = y1，.，y h.最后，给定一个函数f：A→B和y∈A，f−y：A\y→B定义为f−y（x）=f（x），对所有x∈A\y。表A.1中最重要的规则是（合并1）和（合并2）。它们调节节点如何融合。规则（merge1）融合两个节点，前提是其中一个节点上不需要约束，而规则（merge2）处理需要互补动作的节点。最后，规则（par）说明了如何将不相交图上的转换组合在一起。规则（merge 1）融合节点x和y，前提是没有对y施加约束，即Λ（y）↑。假设xπy<$π（y）/= y强制，如果y与节点x融合，使得xπy（即x和y在同一等价类中），则y一定不是代表元素。然而，如果x/πy融合[x/y]是可能的;事实上，条件xπy<$π（y）/=y平凡地成立。94E. Tuosto/Electronic Notes in Theoretical Computer Science 112（2005）77►►从Γ，y G的过渡可以重新公式化以获得y和x合并的过渡，条件是它们的代表元素ρ的融合反映在Λ、π和延拓ΓJGJ上。 如果y与 x，与它们等价的其他节点也是融合的;（merge1）结论中的融合替换是π;ρ（限于Γ），π（y）的所有出现都被n（Λ）中的π（x）替换，最终图是ρGJ。它是通过合并GJ中的π（y）和π（x）得到的。规则（合并2）补充动作。该规则允许在转换中合并x和y，如果它们有互补的动作。对于（merge1），x不能替换其等价类的代表元素最一般的单位器ρ考虑了在[x/y]被替换后，由于替换[v/u]的传递闭包而可能产生的等式。ρ融合约束的对应节点并传播先前的融合π。得到的约束ρΛε {（x，τ，τ ε）}不改变在与x和y不同的节点上施加的约束（直到必要的融合ρ）。熔合代换（π;ρ）−y通过应用ρ作用于Γ。最后，节点U是那些既不在（π;ρ）−y（Γ）中也不是由ρΛ生成的节点，它们被限制在ρGJ中;这对应于π-演算的封闭观察A.1我们注意到规则（merge 1）和（merge 2）中提到的节点x是出现在规则中的Γ中的节点。对于条件xπy <$y/= π（y），这是紧接着的。规则（par）简单地将不相交的判断组合在一起。 条件（Γ 1 <$Γ2）<$（ΓJ1<$ΓJ2）=<$;证明了π<$πJ是定义于dbecauseit的，意味着Γ 1 <$Γ J1=<$，而且这样的条件表明，• 图Γ1<$G1和图Γ2<$G2是不相交的;• 由Γi<$Gi（i∈ {1， 2}）的转移生成的名字既不作为另一个图的名字出现，也不作为它的转移生成的名字出现应用于节点x的函数π<$πJ是π（x）或πJ（x），取决于x∈ΓJ。注意，π<$πJ定义得很好，因为Γ <$Γ J= π。