网络意识的π演算-糕点模型下的P2P路由机制验证

可在www.sciencedirect.com在线获取理论计算机科学电子笔记312（2015）3-17www.elsevier.com/locate/entcs网络感知的π演算-糕点模型1Ugo Montanari乌戈·蒙塔纳里2，4 MatteoSammartino马特奥·萨马蒂诺2，3摘要对等（P2P）系统为分布式应用程序的执行提供了网络基础。 它由通过覆盖网络进行交互的对等体组成。覆盖网络是高度动态的，因为对等点可以随时加入和离开。传统的过程演算，如π演算、CCS等，似乎是不够的捕捉这些类型的网络，它们的路由机制，并验证它们的属性。为了为了以更明确的方式建模网络架构，在[14，18，15]中，我们介绍了网络意识π演算（NCPi），这是π演算的扩展，其名称表示网络节点和链路。在[15]NCPi（的一个简单版本）已经配备了一个共代数运算模型，沿着Fiore-Turi基于前片层的方法[6]，并配备了一个等效的历史相关自动机[13]，即，一个（通常）适合验证的有限状态自动机在本文中，我们首先给出这些结果的简要说明然后，我们的贡献是一个NCPi表示的p2p架构糕点草图。特别是，我们给它的覆盖网络和分布式哈希表建立在它上面的模型，我们给他们的正确性的证据，证明收敛的路由机制。关键词：对等，路由，覆盖网络，分布式哈希表，糕点，验证，路由收敛，进程演算，网络意识的pi演算，预层，余代数，HD自动机1介绍对等（P2P）系统为分布式应用程序的执行提供了网络基础。它是由对等点组成的，这些对等点通过建立在物理网络之上的应用层覆盖网络进行覆盖网络是高度动态的，因为对等节点可以随时加入和离开它，这会导致其拓扑结构的不断重新配置。一个关键的属性是路由机制应该在每次重新配置后都能工作。传统的进程演算，如π演算[12]，CCS [11]和其他，似乎不足以描述这些类型的网络，它们的路由机制，1由欧盟综合项目257414 ASCENS和意大利MIUR项目CINA（PRIN 2010）2比萨大学计算机科学系意大利3电子邮件地址：sammarti@di.unipi.it4电子邮件：ugo@di.unipi.ithttp://dx.doi.org/10.1016/j.entcs.2015.04.0021571-0661/© 2015由Elsevier B. V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。4联合蒙塔纳里湾Sammartino/Electronic Notes in Theoretical Computer Science 312（2015）3验证其属性。事实上，它们从网络细节中抽象出来，因为两个进程只允许通过共享通道进行通信为了以更明确的方式建模网络架构，在[14，18，15]中，我们引入了网络意识π演算（NCPi），这是π演算的无缝扩展，具有网络的自然概念：节点和链路被视为可以创建，传递和用于传输的计算资源，因此它们被表示为名称，遵循π演算方法。NCPi的主要特点如下。• 有两种类型的名称：站点，这是网络的节点，和链接，命名为站点对之间的连接器。站点只是原子，例如a，链接的形式为lab，这意味着从a到b有一个名为l的链接。• 该语法可以通过限制操作符表示链接的创建，以及通过专用前缀在链接上激活运输服务。分离这些操作与π演算一致，其中创建和使用通道作为主体是两个不同的操作。此外，进程不需要在共享信道上通信：引入了一个扩展的输出原语，指定了发射和目的地。• 观察的语义表示并发传输的路由路径的多集的形式。这遵循了这样的直觉：流程应该以真正分布式的方式运行，而没有一个中央协调器来对它们的操作施加交错的顺序相关的行为等价对于语言的所有运算符都是封闭的，包括输入前缀，即它是一个同余。此外，操作语义配备了一种机制，用于根据用户定义的策略控制路由路径的推理这允许实现路由算法。方便的是，在[15]中，我们已经引入了一个基于预表的共代数语义，NCPi，以[6]的风格[6]的基本思想是有一个模型，我们区分：(a)资源域，（b）程序域和（c）资源和程序之间的“映射”域。在NCPi中，一个进程的资源是它的自由站点和链接，描述了它的通信网络。因此，（a）是G类合适的图，表示网络，配备有添加新顶点和边的内函子，建模网络资源分配;（b）是Set，其中某些对象被视为NCPi过程的集合;（c）是函子G→Set（G上的预层），将每个网络与NCPi进程集关联这样的网络。然后，将操作语义建模为余代数[17]由于状态在一个预层中，因此每个状态都用它的网络来修饰：这使得网络资源分配沿着转换的显式表示成为不幸的是，我们仍然有无限多的状态，因为分配的资源可能无限增长，即使只有有限的一部分实际上是可访问的，例如，在递归过程中进行挤压。然而，我们的状态预层是HD-自动机是分配和释放自动机，联合蒙塔纳里湾Sammartino/Electronic Notes in Theoretical Computer Science 312（2015）35过渡。它们允许最小的，可能是有限的状态，代表，其中所有的双相似状态都被识别，可以像[5]中所示和实现的那样计算。本文的第二部分是对NCPi语法和语义的概括。主要贡献是第3节，为了展示我们语言的表达能力，我们提出了p2p架构Pastry的NCPi模型[16]。该模型是在FP7自主服务组件集成（ASCENS）项目的背景下设计的，其中在云计算案例研究中采用了Pastry的路由功能。详情可参见[18，第6章]。在Pastry中，peers有唯一的标识符，逻辑上排列在一个环中。主要的操作是按键路由：给定一个消息和一个目标键，消息被传递到标识符在数字上最接近键的对等体。Pastry通常用于实现分布式哈希表（Distributed Hash Tables，DHT），即哈希表，其条目分布在对等点之间：在此上下文中按键路由相当于哈希表查找。我们的糕点模型如下。我们首先形式化的特点，糕点路由，确保其收敛。这些在[16]中有非正式的陈述，但我们需要一个严格的公式，这样我们才能证明我们模型的正确性。然后我们给出了一个Pastry对等点的NCPi实现。其基本思想是将标识符捕获为站点，将覆盖网络捕获为对等点之间的链接集合我们对对等体的路由数据结构及其操作、由于加入对等体而引起的重构以及向应用程序提供路由功能进行建模节点加入会触发一个复杂的过程，最后会创建来自/到加入对等体的新链接。我们表明，由此产生的覆盖仍然保证路由- ING收敛。最后，我们建立了一个简单的分布式哈希表模型，其中查找表示为从调用查找的对等体到负责目标键的对等体的路由路径。这些路径是由节点提供的原子转发服务组合而成，采用模型提供的机制实现路由协议。我们证明，我们有路由收敛也在这种情况下，即，查找总是到达正确的对等体。2网络意识π-演算2.1说明性示例为了更仔细地研究微积分，考虑图1中的系统。其目的是对在运行时确定其拓扑的网络进行建模。我们有一个网络管理器M，能够创建新的链接并授予对它们的访问权，还有两个进程P和Q，它们分别通过a和b访问网络;它们愿意通信，但a和b之间不存在链接，因此P将请求M建立这样的联系。最后，我们有一个链接服务器L，它能够在给定的链接上提供运输服务实际的定义是，M可以在m处接收两个站点，在它们之间创建一个新的链接，并将其从m发送到第一个接收到的站点。注意，输出前缀有三个组成部分，从左到右：发射地点，目的地6联合蒙塔纳里湾Sammartino/Electronic Notes in Theoretical Computer Science 312（2015）3P·M·Md=ef m（x）.m（y）. （lx y）（mxlx y.M）的Pd=efQ d=efL（lxy）d=efama.amb.a（lb（x）。QJlx y。L（lxy）（xy））的。（abc。PJ|L（lxy））Sd=ef P|M|Q|L（la m）|L（lmJa）Fig. 1.示例系统。场地和基准面。进程P可以先将a和b从a发送到m，然后等待a处的链接。该链路与其端点一起被接收，因为a和b在（l（ab））中绑定。这个过程变成了两个组件的并行组合：第一个组件可以将c从a发送到b;第二个组件调用过程L，其功能是激活链接lab。这种激活被表示为链接前缀lab。在L的定义中：当消费时，它在lab上产生运输服务，其可以由执行上下文使用（即，通过其他进程并行）将数据从a转发到B.链接前缀表示链接的单次激活，就像π演算中的输入/输出前缀表示其主题通道的单次使用一样。这解释了L的递归定义，它旨在对持久连接进行建模过程Q只是等待b处的数据。最后，整个系统S是P，Q，M和两个进程的并行组合，这两个进程在a和m之间建立了双向持久连接。在展示一些计算步骤之前，我们通过与π演算的比较来简要介绍观察结果与π演算一样，我们有表示输入、输出和完整通信的观测。但是，由于NCPi允许远程通信，因此它们都包含通信中遍历的链接序列（可能为空）。例如，进程P可以在a处发出a，目的地为m，如下所示;AMA−−−−→ amb.a（l（xy））的。（abc。PJ|L（lxy））标签·;ama是零长度（即，具有空的链路序列）输出路径。符号·是语法糖，表示路径的起点。一般来说，在·和ama之间可能有一个链接列表W，这意味着a在被发射之前经过W对称地，M可以在m处接收具有目的地m的数据amma;−− − −→m（y）。（lay）malay. M其中，是（零长度）输入路径。mma中的前两个站点，即联合蒙塔纳里湾Sammartino/Electronic Notes in Theoretical Computer Science 312（2015）37·）上午）·am−−−−→接收和目的地站点分别重合，因为路径表示本地输入，类似于早期的π演算输入动作ma。在这里，对于任何mJ，mj之间的链路的列表W，并且将意味着W可以被用来从mJ到达目的地m。在引入表示完全通信的路径之前，我们引入服务路径，这在π演算中没有对应物服务路径具有a;W;b的形式，其中W是链路的序列。它表示一个传输服务，执行上下文可以使用该服务将数据从a路由到b。例如，L（我是a;l;m−−−−−→ L（lam）其中a;lam;m是从a到m的运输服务。最后，我们有了完全通信，用一条完全路径·;W;·表示。与π演算τ作用量不同，这种观测不是沉默的，因为我们允许观测传输数据的路径W;数据本身仍然是不可观测的。另一个不同之处是，一个完整的路径通常是由多个同步产生的，每个同步都连接了一对兼容的路径。例如，为了使P向M传送a，P和L之间必须有第一个同步（lam）。P|L（我是;l;mma−−−−−−−→ ...其中·;lam;mma是·;ama和a;lam;m的级联。这些路径兼容，因为前者在后者转发数据的站点处发射其数据，即a.它们的连接表示使用lam将a从a转发到m（实际上，新的发射位点是m）。这里的延续是上面所示的延续的平行组成 一个完整的路径是由P之间的另一个最终同步产生的。|L（lam）和MP|L（我是）的方式|我是...这意味着已经通过我进行了一次完整的通信。现在我们概述整个系统S可以执行的步骤：(i) P向M传送要创建的链路的端点a和b：它被观察为·;lam; ·的两个连续出现。在这种相互作用之后，系统的状态是a（l（x y））。（abc。PJ|L（lx y））|（la b）（mala b .）M）的|Q|L（la m）|L（lmJa）.(ii) 马勒湾M 通信 labto a（l（xy））。（abc。PJ|L（lxy））：观察结果为•;lmJa;·，并且结果状态为（la b）（abc. PJ|L（la b）|M）的|Q|L（la m）|L（lmJa），其中l ab的范围已经扩展。(iii) ABC. PJ将c传递给Q：在这种情况下，尽管lab用于传输，但只能观察到·;·，因为这种链路是受限的。这类似8联合蒙塔纳里湾Sammartino/Electronic Notes in Theoretical Computer Science 312（2015）3J到π演算τ作用。延续是（la b）（PJ|L（la b）|M）的|QJ[c/x]|L（la m）|L（lmJa）.2.2微积分概述在这里，我们给一个简要概述的微积分。我们假设有两个可归集S和L的网站和链接，分别;L配备了两个功能 s，t：L → S，表示每个链接的源和目标。我们用lab表示一个链路l，使得s（l）=a，t（l）=b。定义2.1NCPi过程定义如下，对于a，b∈ S，lab∈ L：p：：= 0 |π.p|p + p |p |p|（r）p|A（r1，r2，...， rn）r：：= a|labs：：= a |l（ab）π：：= abr|a（s）|LAB|τA（s1，s2， . ，sn）d=ef pi/=j=n（si）n（sj）=其中n（a）={a}且n（lab）=n（l（ab））={lab，a，b}。NCPi进程的语法扩展了π演算的语法如下。限制（r）p可以约束一个站点（r∈S）或一个链接（r∈ L）。除了发射地点a和基准点r之外，输出前缀abr还指定了目的地地点b。输入a（l（ab））可以表示链路及其端点的接收。链接前缀lab.p意味着这个过程可以将数据从a通过l传输到b的服务提供给执行上下文，然后可以作为p继续。过程定义的形式参数不能共享名称。自由名fn（p）如预期的那样由递归定义。我们简要描述一些有趣的案例。如果lcd不是p中的顶级约束或输入绑定器的参数，即p的形式为ablcd.pJ或lcd.pJ，则fn（p）包括{lcd，c，d};否则，lcd是绑定的，但其端点可以是自由的，例如fn（（lcd）pJ）={c，d}{fn（pJ）\{lcd}. 结合位点的情况，例如p =（a）pJ，需要一些注意，因为p中与端点a的自由链接在p中成为隐式绑定;为了避免这种情况，我们排除了一些非良构过程（参见[15，3.1]了解详细信息）。过程的结构同余包括通常的交换monoidal律，|和+，α-转化率w.r.t. 绑定的站点和链接，以及过程定义的展开在上一节中，我们已经看到了单个路由路径作为观察，但语义允许以多路径集的形式并行观察多个路径。例如，我们可以观察到图1中的S做·;ama|我是|mma; ·，其表示三元素多重集。定义2.2定义了路径（记为α）和路径的多集（记为Λ），联合蒙塔纳里湾Sammartino/Electronic Notes in Theoretical Computer Science 312（2015）39p·|1p·||2−−−−→1如下所示α：：=a;W;b（服务路径）|·; W;·(Complete path)|·; W; abr(Output path)|abr; W;·(Freeinput path)|ab (s); W;·n (s) ∩ (n (W) ∪ {a, b}) = ∅(Boundinput path)r：：= a|labs：：= a |l（ab）W：：= lab|W; W|ϵΛ：：= 1 |α |Λ 1| Λ 2|（r）Λ除了上一节介绍的路径之外，我们还有一个绑定输入路径，表示接收绑定名称。路径的多重集可以是：空多重集1;单点α;并Λ 1|Λ 2和挤出（r）Λ。注意，我们没有绑定输出路径;相反，挤出限制（r）可以在其范围内拥有整个多重集Λ，因为我们允许Λ中的许多输出路径挤出r。我们有一些关于路径和多重集的结构同余公理：路径α是字符串，即，它们形成具有乘法的幺半群;并且单位Λ; Λ是多集，即，它们形成一个乘法交换幺半群|和单元1;挤出限制可以交换，并且它们的范围可以扩展到包括受限制名称不能自由出现的多集。NCPiLTS是从SOS规则集合中派生出来的最小的LTS。我们描述了最有趣的规则，即那些实现进程同步。同步分两步执行路径收集：通过以下规则收集并行进程的路径p1−Λ→1 q1p2−Λ→2 Q2p|pΛ 1|Λ2Q|Q其中Λ1中的绑定名称需要相对于. r. t是新鲜的。p2和Λ2（对于Λ2、p1和Λ1相同）;路径连接：其他规则从上一步产生的多集中挑选两个兼容的路径，并用它们的连接替换它们，而不修改源进程;换句话说，这些规则同步源进程的两个子进程。例如，可以使用以下规则连接具有公共端点的输出路径和服务路径，从而产生扩展的输出路径（R）（;W;abra;W′;cΘ）−→q（R）（;W;W′;cbrΘ）−−→q其中，（R）是一系列限制，Θ是一个没有挤出限制的并发路径（它们都是使用范围扩展在顶层引入的210联合蒙塔纳里湾Sammartino/Electronic Notes in Theoretical Computer Science 312（2015）3的路径多集）。NCPiLTS的双相似性定义如下。它的简单定义类似于π演算早期互模拟，因为如2.1节所述，我们采用早期风格的输入。定义2.3二元、对称和自反关系R是一个网络连接，若（p，q）∈R且p−→ΛPJ，其中hbn（Λ）为零，则为一个有意义的二等分. q，意味着reisqJ使得q−→ΛqJ且（pJ，qJ）∈R. 双相似性是最大的关系，并表示为CNONC。该关系具有以下重要性质。定理2.4 NCPi算子是关于所有NCPi算子的同余。直观地，该性质成立，因为观察Λ允许区分具有不同并行级别的过程（例如，并行处理及其顺序交织）。NCPi有一个内置的机制来控制路径的推理。事实上，SOS规则非确定性地导出所有可能的路径为了仅选择特定路径，例如根据特定路由策略，可以定义转发谓词：L×S×Proc→ {true，false}然后将其用作执行路径连接步骤的规则的附加附带条件：如果Rlab（lab，c，p）返回true，则路径p具有目的地C1可以与Lab级联。例如，通过这种方式，我们可以根据某些度量（成本、延迟、距离等）排除非最佳链路参见[15，6]，了解对边界网关协议进行建模的转发谓词。3糕点模型在本节中，我们将使用NCPi对Pastry覆盖网络和分布式哈希表（DHT）进行3.1糕点概述Pastry是一种对等体系结构，其中对等点和密钥具有标识符，被视为按顺时针顺序排列在环上。Pastry提供的主要服务是按密钥路由：给定密钥k，Pastry将消息传递给负责k的对等体，即其标识符在数值上比所有其他对等体更接近k的那个路由实现如下。每个具有标识符id的对等体维护两个数据结构：路由表和叶集。路由表包含共享id前缀的对等点。叶子集合包含具有相对于id在数字上最接近的较小和较大标识符的对等体（叶子）。每当id接收到一个带有目标键k的消息时，它会检查k是否属于叶集范围。如果是，则将消息转发到数值上最接近k的叶子（如果该叶子本身不是id否则，使用路由表：下一跳是与k共享最长前缀的对等点。图1中示出了示例系统2，其中标识符是二进制字符串。联合蒙塔纳里湾Sammartino/Electronic Notes in Theoretical Computer Science 312（2015）311路由表1111叶片组11001011路由表10101000叶片组…101110001100R01-11000. 11110011101-11111. 1010001011011图二. 糕点示例系统。例3.1考虑图3中标识符为1010的对等体。 2，假设1100负责密钥1101。来自1010的具有目标键1101的消息如下路由。 由于1101不属于1010的叶集所跨越的区间[1000，1011]，因此使用路由表：1010和1101共享的最长前缀为1，因此消息被转发到信元（1，1）中的对等体，即1111。 一旦1111接收到消息，它发现1101在它的叶集范围内（叶集将1111本身作为上限，因为没有具有更大标识符的对等体），所以它将消息转发到最接近1101的叶，即1100。Pastry路由过程的一个重要属性是收敛性：消息最终到达目的地。[16，2.2]中陈述了这个性质，但只是用非正式的术语。在这里，我们提供了一个正式的，数学的帐户，为了来证明我们模型的正确性设x，y为两个标识符。我们将x和y之间的环距离dr定义为环上x和y形式上，如果I是标识符空间的大小，我们有d（x，y）=.I−|x−y||>[ I / 2]|>[I/2♩|否则|otherwise第一种情况发生在x和y的数值距离大于环的一半时：那么我们必须考虑互补弧。属性3.2（路由收敛）路由过程总是收敛的：给定一个带有目标键k和对等体id的消息，要么id负责k，要么它可以将消息转发给idJ，使得dr（idJ，k） shl（a，k）如果aob=k图三. 糕点转发谓词。引入一种新类型的链接：aok意味着标识符为a的对等体负责密钥k。Pastry路由策略通过转发谓词Pastry实现，如图3所示。我们用shl（x，y）表示x和y共享的最长前缀的长度，用xl表示标识符的顺序关系，视为自然数。第一种情况允许经由a的叶集中的链路将具有目标k的消息从a转发到b，条件是：（i）没有比b更接近k的其他叶b j;（ii）a具有两个叶b 1和b 2，在a的相对侧（但不一定与a不同）第二种情况允许通过路由表中的链路进行转发，只要叶集中没有更好的链路，并且到达的对等体的标识符b与k比a多共享（至少）一个数字。第三种情况处理允许通过负责它的对等体到达密钥k请注意，路由机制与联接过程相同。观察结果是单跳，因为在每次转发时需要执行一些操作。在这里，相反，一个单一的观察描述了所有的路由步骤。我们可以在Pastry系统上建立一个分布式哈希表，a1，.，N如下。假设分布式哈希表有m个键值对ki，vi，设aki为⎟⎟⎠⎟⎠14联合蒙塔纳里湾Sammartino/Electronic Notes in Theoretical Computer Science 312（2015）3DHT1nk k·负责ki的对等体的标识符，即， 在1，...， 一个;DHTd=efHd=ef条目（k，v，a）d=ef同级（a1）|......这是什么？ |H|H条目（k1，v1，ak1）|......这是什么？| k（b）. abv.|k (b).abv. 条目（k，v，a）这里H表示处理表其思想是将针对密钥k的DHT查找请求实现为目的地为k的消息，携带发送方的标识符b在接收到该消息时，处理程序Entry（k，v，a）fork，v用包含v的消息回复b。注意，Pastry中的节点连接可能会在DHT中引入新的键值对。然而，为了简单起见，我们假设DHT是固定的。添加一个值为v的键k可以通过使用路由机制来建模，以找到idak最接近k的对等体，然后产生一个新的进程Entry（k，v，ak）。我们在此场景中提供属性3.2a;aQb;b引理3.3对于每个对等点a和密钥k，存在DHT−− −→DHTJ，其中D∈{k，0}，使得b=k或b比a更接近k，即a、b、k满足Prop。3.2.下面的结果是引理3.3和Pastry的定义的直接结果。它说，给定一个密钥k和一个对等体a，总有一条路径从a路由到k的查找请求。定理3.4设k是DHT中的密钥，ak是对它负责的节点。然后，对于每个对等点a，存在一个转换a; aQa;. aQa;aBk;−−−−−−−−−−−−−−−→ DHTJ其中D ∈ {n，©}且n ≥ 0。作为示例，我们示出了如何在图2的系统中计算路由路径。为了简单起见，让我们考虑一个只有一个键值对（1101，v）位于1100的分布式哈希表：Hd=ef1100o1101|1101（a）。1100av. HDHTd=efSys|H其中Sys在第3.2节中定义。考虑以下过程，其表示在1010应用d=有效 101011011010. 1010（vJ）。Ap pJ（vJ）.该过程发送对键1101的查找请求，接收结果并将其用于某些计算。所以我们有•电话：1010 1101 1010J J JApp−→1010（v）。App（v）.此请求的路由步骤与例3.1相同。在这方面，他们联合蒙塔纳里湾Sammartino/Electronic Notes in Theoretical Computer Science 312（2015）315H·App|··双氢睾酮111111011100101110101000图四、在图1的系统中，用于密钥1101的来自1010的路由路径二、成为以下的，描绘在图。41111; 1111−−→同伴（1010）1111; 1111 1100;1100−→同伴（1111）对于键1101，应用于Peer（1010）和1010© 1111以及Peer（1111）和1111©1100的谓词Pastry为真，因此我们可以使用SOS规则来连接到目前为止所示的三条路径（参见2.2节中描述的连接步骤）。结果是•电话：+86-110 - 8888888传真：+86-110 - 8888888可以推断1100B 1101;−→1100 1010 v. H.最后，我们可以将所有这些路径连接起来，得到;1010©1111; 1111 1100;1100B1101;−−−−−−−−−−−−−−−−−−−−−−−→ 1010（vJ）。App（vJ）|Sys |1100 1010v. H其展示了从1010到1100的整个路由路径。最后，假设覆盖网络具有返回到1010的路径，则达到应用程序（v）|DHT。4结论在本文中，我们提出了NCPi，π演算的扩展与明确的网络的概念。为了实现这一点，我们用命名连接器丰富了语法，并定义了一个LTS语义，其观察结果是路由路径的多集。语义的并发性质使得双相似性成为一致性。我们使用NCPi对Pastry的对等架构进行其优点在于，可以将用于DHT查找操作的路由路径观察为通过覆盖的整个路由路径，这是由对等体之间的多个同步引起的同行（1010）中国人（1111）16联合蒙塔纳里湾Sammartino/Electronic Notes in Theoretical Computer Science 312（2015）3未来的工作包括使用NCPi来模拟其他网络场景，例如社交网络。我们还计划通过建模来扩展Pastry场景一个现实生活中的应用程序，例如文件共享，它采用了分布式哈希表操作。我们还可以在链接中添加定量信息，例如，成本、带宽等，以便捕获QoS或类似要求。与我们最密切相关的工作是[7]和[3]，其中提出了Dπ[10]和KLAIM[2]的网络感知扩展，分别称为DπF和TKLAIM它们的网络表示与我们的网络表示非常不同：在DπF中，位置通过类型系统与它们的连通性明确地联系在一起，KLAIM有一个特殊的过程来表示连接，而在我们的微积分中，连接只是名称，因此可用的网络节点和连接对应于自由名称的标准概念。这带来了更简单的原语，但也带来了更高级别的二进制性：可以在进程之间创建和传递连接，如说明性示例所示至于我们的Pastry模型，它在DπF和TK中不容易实现：网络在这些演算中总是可用的，而我们通过链路前缀控制叶集和路由表链路的激活; DπF和TK不允许观察多跳路径，而我们能够将DHT查找表示为通过覆盖的路由路径。我们也可以引用[8，9，4]作为微积分的例子，其中资源携带一些额外的信息。见[18，7.1.1]详细比较。引用[1] Cristenzo Ciancia，Alexander Kurz和Ugo Montanari。作为资源绑定有效模型的对称性族。ENTCS，264（2）：63[2] Rocco De Nicola，Gian Luigi Ferrari，and Rosario Pugliese. Klaim：一种用于代理交互和移动性的内核语言。 IEEE Trans. 软件工程师，24（5）：315[3] Rocco De Nicola，Daniele Gorla和Rosario Pugliese。全球计算微积分的基本观测量。 INF. Comput. ，205（10）：1491[4] Edsko De Vries，Adrian Francalanza和Matthew Hennessy。关于显式资源管理的推理（扩展抽象）。在PLACES 2011中，第15ETAPS，2011年4月[5] 吉安·路易吉·法拉利，乌戈·蒙塔纳里和埃米利奥·托斯托。 的HD-自动机的余代数极小化 使用多态类型的pi演算T h e o r . Comput. Sci. ，331（2-3）：325[6] 马塞洛·菲奥雷和丹尼尔·图里。名称和值传递的语义。2001年法律调查，第93-104页。IEEE计算机学会，2001年。[7] 阿德里安·弗兰卡兰扎和马修·轩尼诗在节点和链路故障情况下的系统行为理论。 INF. Comput. ，206（6）：711[8] 马修·亨尼西 计算成本的微积分。 LMCS，7（1），2011年。[9] 马修·亨尼西和曼尼什·高尔。在picalculus（扩展抽象）中计算成本。ENTCS，229（3）：117[10] 马修·亨尼西和詹姆斯·莱利移动代理系统中的资源访问控制。信息计算，173（1）：82[11] 罗宾·米尔纳 通信系统的微积分，LNCS第92卷。 Springer，1980年。[12] 罗宾·米尔纳，约阿希姆·帕罗，大卫·沃克。移动过程演算，I/II。信息计算，100（1）：1联合蒙塔纳里湾Sammartino/Electronic Notes in Theoretical Computer Science 312（2015）317[13] 乌戈·蒙塔纳里和马可·皮斯托雷π-演算的结构余代数与极小hd-automataTheor. Comput. Sci. ，340（3）：539[14] Ugo Montanari 和 Matteo 萨马蒂诺网络意识π演算：并发语义学。ENTCS，286：291[15] 乌戈·蒙塔纳里和马特奥·萨马蒂诺一个网络意识的π-演算及其余代数语义。Theor. Comput. Sci. ，546（0）：188[16] 安东尼岛T.作者声明：by Peter Druschel. Pastry：用于大规模对等系统的可扩展、分散的对象定位和路由。在Middleware，第329[17] 简·J·M·M.拉顿泛余代数：系统理论。 Theor. Comput. Sci. ，249（1）：3-80，2000.[18] 马特奥·萨马蒂诺一个面向全局计算的网络感知进程演算及其分类框架。博士论文，比萨大学，2013年。见http://www.di.unipi.it/www.example.com~sammarti/publications/thesis.pdf。