并发约束编程中的动态空间及其在安全协议和分布式系统中的应用

∃∀可在www.sciencedirect.com在线获取理论计算机科学电子笔记305（2014）103-121www.elsevier.com/locate/entcs并发约束编程中的动态空间[编辑]卡洛斯·奥拉特1DeartamentodeElectronica和计算机科学在庞蒂菲西亚大学Javeriana-Cali，哥伦比亚EscoladeCienciaseTecnologia巴西北纳塔尔格兰德河联邦大学Vivek Nigam2DeartamentodeInformaticaUniversidadeFederaldaParabaJoaoPessoa，Brazil伊莱恩·皮门特尔3DepartamentodeMatem'atic米纳斯吉拉斯联邦大学贝洛奥里藏特分校，巴西巴西北纳塔尔里奥格兰德联邦大学摘要式并发约束编程（Concurent constraint programming，CCP）是一种并发的声明性模型，其中代理通过在共享的部分存储中发布（告诉）和询问约束来相互信息。随着安全协议、社交网络和云计算等新兴应用的出现，CCP模型已经在不同的方向上扩展到以下系统的忠实模型：（1）它已经被证明是一个传递名称的学科，其中代理可以传递本地名称，而不是本地名称。它可以通过局部（）进程与通用（）量化查询的相互作用来描述。该策略已被用于实例中，以模拟新值（nonce）的生成和通信在移动反应式系统中作为安全协议;以及（2）CCP中的底层约束系统已经通过用于分布式空间的规范的本地存储而得到增强。然后，允许代理人共享该文件。与他人分享一些信息，但为自己保留一些事实。最近，我们已经表明，通过考虑一个约束系统，局部存储可以在CCP中neatly表示，其中约束是由具有次指数的线性逻辑（SELL±）的片段构造的。 在本文中，我们将探讨存在主义（）在SELL±中对次指数进行通用（A）量化，以使CCP具有通信位置（空间）名称的能力。由此产生的CCP语言是一种分布式计算的模型，在这种模型中，它有可能动态地建立新的共享空间进行通信。因此，我们扩展了（1）中实现的移动性排序-对于变量-以动态地改变共享空间。代理-（2）以上。最后，我们认为新的CCP语言可以用在面向服务的计算系统的规范中。关键词：并发约束编程，线性逻辑，次指数，移动性，分布式空间。http://dx.doi.org/10.1016/j.entcs.2014.06.0081571-0661/© 2014 Elsevier B. V.保留所有权利。104C. Olarte等人。理论计算机科学电子笔记305（2014）1031介绍性现代并发系统的规范常常要求合理地使用不同的模态排序，例如时间、空间，甚至是代理人的认识状态，等等。[10]逻辑和证明理论常常启发了许多这样的形式主义的 设 计 。 [10] 例 如 ， Saraswat 和 Rinard 在 [25] Concurrent Constraint Pro-gramming（CCP）[23，26]中提出了一种并发模型，它将过程计算的传统操作视图[14]与基于逻辑的声明性视图相结合。CCP中的代理通过告诉和询问表示为对全局存储的约束后来，Fages等人。 在[6] 受 线 性 逻 辑 [8] 和 线 性 逻 辑 编 程 [11] 的 启 发 ， 提 出 了 线 性 并 发 约 束 编 程（LCC），允许使用线性约束，即一旦代理使用的约束就从全局存储中删除。[9]另一方面，Saraswat等人提出了定时CCP（tcc） [24]，这是CCP与时间模态的扩展。最近，Knight等人 [12]提出了另一种具有空间（sccp）和认识（eccp）模态的基于CCP的语言（参见[20]对CCP技术状态的调查另一方面，我们在[18]中已经表明，空间、时间和认识模态可以在一个称为SELLA的单一逻辑框架中统一地指定。证明系统SELLA是SELL（具有次指数的直觉线性逻辑）的扩展，具有一对关于次指数的Quantifier，即A（universal）和A（existential）。这些量化器允许对现有数量的CCP语言进行编码，而这些语言在其他逻辑框架中似乎是不可能的，如[28，3]。事实上，将次指数视为"位置"的观点极大地增强了与之相关的逻辑框架的力量，在这种情况下是线性逻辑。 此外，对地点进行推理的能力似乎是最重要的这是在CCP中捕获不良行为的关键。特别地，上面提到的量化器允许使用任意数量的次指数，这在[18]中描述的编码中起着重要作用。例如，它们被用在模态的无界嵌套的建模中，这是涉及空间和认识信息的系统的一个共同特征次指数的另一个重要特征是，它们可以被组织成一个预先确定的顺序，这指定了它们之间的可测性关系。通过使用与次指数相关的适当预序的量化器，有可能以声明性的方式指定代理人可以操纵信息的规则：边界自然地由次指数的预序所事实是，[18]中的结果为所提到的模态的系统的规范和验证开辟了许多可能性，这是一个很好的例子。例如，当[12]中的一个假设有有限数量的代理时，似乎有可能扩展这些系统，以便通过位置上的量化来处理无限数量的代理。此外，约束的线性度可以直接向前包括在这些约束中。1电子邮件：carlos. gmail.com2电子邮件：vivek. gmail.com3电子邮件地址：elaine@mat.ufmg.brC. Olarte等人。理论计算机科学电子笔记305（2014）103105系统，用于表示可以更新/更改分布式空间内容的代理（对于实例）。此外，通过改变较低的次指数结构，可以将不同的模态置于建模者和程序员的手中。最重要的是，现在有可能使用所有的线性逻辑元理论来推理这样的系统。总之，我们可以总结在[18]中完成的工作{l，e，s，t，ck}−CCP=▶SELLA其中{l，e，s，t，ck}-CCP代表CCP中的线性、认识、空间、时间和公共知识模态。当前的工作正朝着相反的方向移动：SELLA =†？-CCP也就是说，我们问自己，如果我们用次指数学科丰富了这个模型的基本理论，那么CCP中可以指定什么样的有趣特征。在这个方向上至少有两种方法可以可以探索的一个方面是，在SELLA中提出丰富的次指数特征，但它们具有不同的计算行为。例如，似乎如果初始签名是[0， 1]区间，则相应的计算具有概率性flavor[0，1]。人们常常会认为更精细的拓扑空间是特征，例如希尔伯特空间，在另一边实现了有趣的并发系统。然而，在目前的工作中，我们将探索由SELLA驱动的另一个可能的方面：通信结构的可重构性，又名移动性。事实上，与其寻找最初的次指数特征，我们将把注意力集中在次指数上的量化上，而不是寻找最初的次指数特征。也就是说，我们将展示由存在量化（A）创建的新的次指数如何被用作私有位置，这些私有位置可以通过通用量化（A）与其他代理进行通信和共享在CCP语言的上下文中，这让人想起Olarte和Valencia在Universal Timed CCP（utcc）[21]中提出的名称传递规程（用于第一阶变量），其中使用局部（）过程来创建可以通过通用量化查询（）访问的nonce（新鲜值）。本文的其余部分按以下方式组织。在第2节中，我们回顾了[18]中提出的SELLA然后，我们扩展了[6]中的线性约束系统，以考虑SELLA的一个片段中的公式。我们将证明，操纵这样的约束的进程能够表示当前和分布式系统中的感兴趣的行为。我们依靠[18]中的结果表明，这里提出的CCP语言的操作语义具有很强的充分性（在派生级别），并在SELLA中进行了证明。第4节结束了本文。106C. Olarte等人。理论计算机科学电子笔记305（2014）1032线性逻辑和次指数量化器[编辑]我们回顾了Girard的ILL的! ，？; 4和单元1、T和0。这是由于指数!，我们可以在线性逻辑中区分两种形式--在左边的上下文中：主要连接的线性单元不是A !和那些没有界限的人谁的主要联系是一个!这就引出了指数在逻辑等价关系方面是不规范的。事实上，如果出于任何原因，我们决定用标准规则定义蓝色连词和红色连词（分别为b和r）：A，B−→C−bL−→A−→BTBRAbB→C→AbBA，B-→C rL-→A-→BR RRRArB→C r B→A rB因此，很容易证明，对于任何公式A和B，AbBA rB。这意味着直觉合取的所有符号都属于同一个等价类。[10] 然而，我们可以选择使用任何特定颜色的连词作为其规范形式，并且这种选择并不表示可证明性然而，同样的行为并不适用于线性逻辑指数。事实上，假设我们有红色! R和蓝色!b具有标准线性逻辑规则的指数：! rχ−→FRRF−→C →! bΓ −→ Fbbbχ，F−→Cb! #! F!RR啊!RF→C!RL! R! #! F啊!b! LF→C在这种情况下，我们不能显示! RF惊呼! BF.这就打开了定义指数类的可能性的大门。形式上，具有次指数的直觉线性逻辑（SELL）与ILL共享所有连通性及其推理规则，除了指数：而不是具有单个指数对!和？，SELL可以包含许多标记的指数，例如! L，？我，如所需。 这些被称为次指数[4]。 次指数特征的定义Σ=I，≤，U是从一组标签I构造的，U I是一个指定的集合，其中次指数允许序列左侧的弱化和收缩，并且≤是I的元素之间的前置顺序。我 们 假设U是闭的wrt ≤，即U。，如果a≤b，则b≤U。次指数的引入规则如下所示。对于每一个I，我们添加了与取消推荐和晋升相对应的介绍性规则，其中我们声明4.虽然？它不是ILL的一部分，我们可以添加它的线性版本，不允许它被收缩或削弱。C. Olarte等人。理论计算机科学电子笔记305（2014）103107AA-→明确地说，语言术语的第一阶签名L是L; χ，F−→GaL; ! x1F1，... ! xnF n−→ G aA! LL; χ，! F→G和L; ! x1F1，... ! xnF n-! AG!R规则是什么？A是双重的。 这里，规则! R（和？a（L）对于所有i具有边条件a≤xi。就是这样，一个人只能介绍一个! A在右边（或A？如果序列中的所有其他公式都标记有大于或等于a的索引，则为a（左）。请注意，这意味着向下保留了可证明性：if a formula! aP可以从一组假设中证明，就是这样! bP，对于b≤a。此外，对于所有aDrewU，我们添加了结构规则：A AL; χ，! F，! F→GCL; χ，! F-→G和L; χ −→ GWL; χ，! F-→G也就是说，我们也可以自由地指定哪些指标是无界的（那些出现在U组中的指标），以及哪些指标是线性的或有界的。有关SELL A系统的重点直观版本，请参见作者网页上[18]的配套技术众所周知，当与线性逻辑相比时，次指数极大地增加了系统项的可表达性。例如，次指数可以用来表示证明系统的上下文[19]，标记代理的认识状态[16]，或者指定顺序计算中的位置[17]。与线性逻辑的标准表示法的关键区别在于，虽然线性逻辑只有7个逻辑上不同的bangs和问号前缀，但对于a nnbundednumberofsu c h前缀，SELL all o ws。啊! I或R!我？J. 通过使用不同的前缀，我们能够以更有创造性的方式解释次指数，例如分布式系统中的时间单位或空间和认识模态[18]就目前而言，! iP指定进程P位于空间i中的位置。更多，因为! IPP，P的信息可以传播到空间i之外。 在 另一边，!我？iP指定P位于i，但其信息被限制在空间i中。对SELL中预期模态的解释取决于对次指数进行量化的能力。为此，我们在[18]中引入了包含两种新颖联系的系统SELLA：次指数上的普遍（A）和存在（）量化器。2.1次指数量化器[编辑]从给出前置序（I，≤）的格理论中回忆起来，元素a她家的理想≤I，写成a，是集合{x}|x≤a}。SELLA的次指数签名的形式为Σ =指定不相交的预订单。最后，集合U{f（a）|aιI，fιF}是从族生成的次指数集，因此，它相对于≤向上闭合：if a≤b，其中a，b ιI，and f（a）她家U then f（b）她家U。请注意，SELLA系统是从签名中，判断s：每当s≤a时，a为真。因此，我们得到集合AΣ={s：a |s，a她家，s ≤a}的类型次指数常数。与引入本征变量的通用量化器一样，次指数A的通用量化器引入了次指数变量l：a，其中a是次指数常数，即a是次指数常数。A，A，I。因此，SELL A序列的形式为A; L; χ −→G，其中A = Aσ{l1：a1，...，n：a n}，和{l1，...，l n}是一组不相交的次指数变量和{a1，...，a n}I是次指数常数。从形式上讲，只有这些次指数常数和变量可以作为次指数爆炸和问号的指数免费出现。次指数量化器的引入规则看起来类似于那些引入第一阶量化器的规则，但不是操纵上下文L，而是使用第二阶量化器。他们操纵上下文A，其中l是新鲜的，即，不出现在AnorL和A：A;A：A;L; χ，P[l/lx]−→GA;L; χ，Alx：a.P−→GA，le：a;L; Gamma−→G[le/lx]AA;L; χ−→Alx：a.GRA，le：a;L; χ，P [le/lx]−→GA;L; Gamma，lx：a.P−→GA;L; χ−→G [l/lx]A;L; χ−→lx：a.GR直观地说，次指数变量扮演着与本征变量相似的角色一般变量li：ai表示在次指数常数ai的理想范围内的任何次指数。这是通过构造一个称为序的序来形式化的，写为≤A。这个前置序被正式地用在提升规则的边条件中，并且定义在通过将一个族fi她家她家F应用于I的一个元素而获得的次指数上。从形式上讲，它是下面集合的传递性和反射性闭包。{f（si：a）≤Af（sj：b）|f她家，si，sj她家，si≤sjf（l：a）≤ Af（s：b）|f她家，l/她家，s和a ≤ s。这个集合的第一个分量规定，族仅在涉及次指数常数时保持序≤ in Σ;因此≤ A是≤的保守延拓。第二个分量是有趣的一个，它涉及从变量得到的次指数和从常数得到的次指数：l：a意味着l符合a的理想，如果a≤s，则f（l：a）≤ Af（s：SJ）。注意f（li：ai）andf（lj：aj）a与twodi ere ntsu bex pone ntialsvariablesli无关ALLC. Olarte等人。理论计算机科学电子笔记305（2014）103109是的DAbD：DA：ALx：aL和：Ab：aSignature（I，≤）类型子表达式。 （A，≤A）图1。a，b，d她家和f（b：a）表示a和f（b：a）≤Af（a：a）的理想中的任何次指数常数。lx，ly是类型a的次指数变量。注意f（l x：a）≤Af（a：a）≤Af（d：d）。还注意到f（lx：a）/≤Af（ly：a），即v变量，e v在相同的t和pe中，是不相关的w. r. t≤A。和lj（见图1）。preorder≤A用于bangs的右引入和问号的左引入，其方式与SELL中的preorder ≤ A类似。A; L; ! f（l1：a1）F1，... ! f（ln：an）F n−→ GA;L;! f（l1：a1）F1， . . . 啊! f（ln：an）Fn−→f（l：a）G! F（L）RA;L;! f（l1：a1）F1， . . . 。 ! f（ln：an）Fn， P−？f（ln+1：an+1）GA;L;! f（l1：a1）F1， . . . 啊! f（ln：an）Fn，？f（l：a）P−？f（ln+1：an+1）G？F（L）L边条件为对于所有1≤i≤n+ 1，f（l：a）≤Af（li：ai），其中≤A是由特征符号Σ和A构造的序序，如上所述。请注意，bangs和问号使用族，而Quantificers仅使用常量和变量（即，类型为次指数）。这种互动让我们可以将公式与不同的族绑定，如公式A1：a中所示。[! f（l：a）P!g（l：a）PJ]。正如[4]中所指出的，对于割除，人们需要小心次指数的结构性属性。对于次指数变量，我们定义f（lii：a）总是有界的，而对于次指数常数，它类似于before：iff（s：a）U，则可以应用结构规则。在[18]中，我们规定销售A允许切割消除。系统。定理2.1对于任何签名Σ，证明系统SELLA允许剪切-删除。在论文的其余部分，我们将简单地写! f（l）而不是! f（l：a）当类型"：a "可以从上下文推断为A l：a时。（! f（l：a）F）。类似于"？"。我们也会写的! S和？当家族和类型不重要或可以从上下文中推断出来时 此外，给出形式为s = s1的次指数序列。·······我们会写!这是卑鄙的!第一章···!sn. 同样的原因？S.110C. Olarte等人。理论计算机科学电子笔记305（2014）103⊗3将A作为约束系统进行销售并发约束编程（Concurrent straint Programming，CCP）[25，23，26]是一种并发模型，它将过程计算的传统操作视图与基于逻辑的声明性视图相结合（参见[20]中的调查）。这使得CCP受益于计算和逻辑过程中的一整套合理化技术，这两种技术都是在计算和逻辑过程中开发的。CCP中的进程通过在部分信息的公共存储中告诉和询问可以作用于的约束过程的类型不是固定的，而是约束系统中的参数。这样的系统可以被形式化为斯科特信息系统，如[26]中所述，或者它们可以被指定为逻辑的适当片段中的公式。如[27，15]中所述。在这里，我们建立在Girard的线性逻辑和线性CCP（lcc）[ 6 ]中公式化的特定约束系统的 更准确地说，我们允许约束条件在销售A的一部分中表述。正如我们稍后将展示的那样，这将带来一种更强大的CCP语言，它能够捕获声明性的分布式空间。此外，新的语言或名称传递学科的原始语言（即，新的语言或名称传递学科）。移动性），包括局部名称（变量）和位置（次指数）。后来，代理人被允许定义共享的通信空间让我们从结束SELL的片段开始，这将作为我们未来的基础。 限制性系统。定义3.1[SELLA-约束系统]一个次指数约束系统（scsforshort）是一个三元组（Σ，C，►Δ），其中Σ是它的bexponentialsignature，其中所有的次指数都是不相关的，除了一个可区分的次指数l∞，它是偏序集Σ的顶部元素。C是由第一阶签名和语法构造的F：= 1 |A| FF| x.F|! S？SF其中A是一个原子公式。 我们将使用c、cJ、d、dJ等来表示C.此外，设Δ是形式为x [c−cJ]的非逻辑公理集，其中c和c j中的所有自由vaRiables都是inx。 WesaythatdentailsdJ，writtenasd►ΔdJ，i}序列C [[Δ]，d −→dJ在SELL A中是可能的（C [[Δ]在定义3.8中稍后陈述）。Weshallomitthe让我们对上面的SELLA片段给出一些直觉。连接器1对应于空存储器，即，这是计算的初始状态连接允许进程将更多信息添加到存储区中。存在主义量化器隐藏了各种变量，使其免受约束。给穆拉的! fj（sj：a）？fj（sj：a）csp说明约束tc在年龄tfj的空间l ocations j中，并且该信息被限定到该空间（参见下面的命题3.2）。最后，C[[Δ]]直观地意味着以Δ定义的公理在系统的所有空间都符号3.1我们将使用[c]s和sc来表示约束!S？sc出于一个美学原因：当约束条件在内部时，将使用第一个符号。C. Olarte等人。理论计算机科学电子笔记305（2014）103111过程，而第二次当他们在商店里。公式[c]s的一个有趣的行为是，它定义了即使可以定义不一致信息的空间。命题3.2（Falseconfineme nt）Let（Σ，Cs，►Δs）beascs，并假设以下序列是可证明的cd−→Δ0。然后，(i) [0]s−→[c]s（如果其局部存储不一致，则可以在空间s中推导出任何c(ii) [0]s/−→ [0]s′ifs/=sJ（在c存在性中是con fined）;(iii) C[[Δ]， [c]s，[d]s−→[0]s（如果空间s同时包含c和d，则它变得不可分辨）;(iv) C[[Δ]，[c]s，[d]s′/−→[0]sifs/=sJ（falseisnotdeducedifcanddareindier空间）;(v) [c] s−→ c（本地信息不是全局信息）。3.1过程的语言。在本节中，我们提出了dccp，这是一种基于CCP的语言，可以通过从次指数约束系统构建的约束来操纵。此语言的主要设计标准如下所示：(i) 分布式代理可以在本地信息对它们是私有的情况下定义。这里的关键方面是在次指数特征中将代理识别为家族名称为此，请注意，两个不同系列的次指数是不相关的，然后，代理的信息将被发送到其本地商店;(ii) 代理可以具有内部结构，也就是说，代理可以具有您的本地商店可以划分为多个位置。为此，我们将在[18]中所做的签名中将这些位置识别为不同的次指数指标。与sccp[12]不同的是，我们将允许无边界和线性位置来指定可以更新信息的空间;(iii) 代理可以交换本地名称，即，这是可能的，以重新配置系统的通信结构。[10]这是通过本地进程和通用定时CCP（utcc）中的通用量化查询的相互作用来实现的[21] ;和(iv) 代理可以创建新的子空间（本地存储）并将其通信给其他代理，从而定义新的共享空间以进行通信。类似于大多数进程计算，dccp功能的进程语言。构造函数的数量很小，并且它强大到足以表达并发和分布式系统的有趣行为。所有基于CCP的语言都通用，我们包括向存储中添加（告诉）新信息、隐藏（本地）变量和并行合成进程的构造。随着lcc[6，10]和utcc[21]的发展，我们允许在查询过程中量化自由变量。此外，如在LCC中，询问代理在由于客户端而演变时消耗信息。112C. Olarte等人。理论计算机科学电子笔记305（2014）103商店的线性性质。在这里，我们注意到，通过改变次指数结构，我们可以指定一些存储是持久的，而其他一些存储是线性的。最后，随着空间CCP（sccp）[12]的发展，我们允许过程被定义为给定的空间（见下面的[P]）。然而，与sccp不同的是，在dccp中，可以创建和通信代理之间的共享通信空间。 后来，我们证明了这种能力不是特别的，因为我们可以给它一个声明性的意义，感谢连接器和A在销售A。定义3.3[dccp的语法]dccp中的进程是从下幂次约束系统中的约束构建的，如下所示：P，Q =告诉（c）|（局部x; l）Q|（absx; l; c）Q| PQ|[P] f（l）|p（x）其中x中的变量和l中的次指数是成对不同的。我们假设对于系统中的每个代理，都有一个唯一的家族名称f，并且Def这样的代理的行为被定义为代理f=P。更多，适用于每个过程name，有一个唯一的定义形式p（x）=ΔP，其中自由变量的集合是x的子集。让我们对上面的过程有一些直观的了解。过程tell（c）将c添加到当前存储d中，生成新存储dc。进程（localx;l）Q创建一组新的变量x和一组新的次指数索引 ， 并宣 布 它 们 对 Q 是 私 有的 。当 这 些集 合 中 的 任 何一 个 为 空 时 ，如 在（localx;√）Q中，我们简单地写（局部x）Q，当没有混淆白羊座。此外，代替（local{x};{l}）Q，我们写（localx;l）Q。如果（分布式）存储在-tailc [y，s/x，l]中，则进程（absx; l;c）Q演化为Q[y，s/x，l]。当这种情况发生时，约束c被消耗掉。 当另一个x或l为空（或单例）时，我们将使用类似于我们对本地过程所做的符号约定。此外，当所有这些集合都是空的时，我们简单地写askcthenQ而不是（absχ;χ;c）Q。然后，abs构造函数可以用作基于约束条件的实现的同步化机制（synchronization mechanism）P和Q的平行组合表示为PQ。进程[P]l执行并在空间l中定义进程P。最后，给出形式p（x）=ΔP的过程定义，t年龄ntp（y）执行pr ocessP[y/x]。在我们进一步讨论之前，让我们注意到，从定义3.3构建的一些进程可能不对于实例，请假设以下代理定义为"定义"。Agentfd=ef（absl;[c]g（l））P在这种情况下，f将查询g的存储中的所有空间，并且它可能消耗来自它的信息。因此，代理f能够直接读取另一个代理的存储。现在考虑一下定义。Agentfd=ef[P]g（l）这里，f能够在g的计算空间中执行过程P。为了避免这种不想要的行为，我们需要对它们施加合成约束，以防止它们发生。C. Olarte等人。理论计算机科学电子笔记305（2014）103113。是的。是的。是的。Σi·iiiiiiiiiiiiiiiiiiixi;lii; χiQ [y/y][l/l];e······f：x;l; χ; Q;d··· ·f：x;l; χ; QJ;dxi;lii;χi，[P]fi（l）;fi（l）difi（x）dj····-→···fi：xi;lii; χi，[P]l;fi（l）di=c中的所有公式都由family索引R···f ：。x; l; Gamma，tell（c）; dΣ··−→···f ：。x;l; χ;dcΣ···泰尔RTDIS· · · · ··· ·fj：xj;lj;χj;dj· · ·fi：xi;lii;χi，tell（[A]fj（l））;di···fj：xj;lj;ghj;djfj（l）A·· ·fi：xi;li;χi;di··· ·j≥ 1。n，xj吵架y = fv（dj）吵架y = fv（χj）吵架y = R打动···f ：。x; l; χ，（局部y; l）Q; dΣ··−→···f ：。xy;l; χ，（局部l）Q;dΣ···Lli+l=≥Rf1：x1; l1; χ1; d1Σ，···fi：xi;li; χi，（局部y; l）Q; diΣ，···fn：。xn; ln; ghn; dnsigma −f1：x1; l1 ≥ l; χ1; d1Σ，···fi：。xi; lii ≥ l; χi，（局部y）Q; diΣ，···fn：xn; ln l; ghn; dnΣdi►c[yJ/y][lJ/l] e。是的。JJΣRA···fi： xi; lii; χi，P; di− →··fi：xi; li; χi，P J; di····。是的。ΣRiiiiiiiiii如果P″ Q和PJ″QJ。xi;lii;χi， P;diΣ−→xJi;lJi;χJi; PJ;dJiΣ。是的。JJJJJΣRSfi（x）djP（x）=ΔPRC···fi ，... fn：≤ ≤;≤;P n; 1>作为系统的初始状态。现在，我们给出一些关于操作规则的直觉：• RTELL：如果c中的所有公式都由familyfi索引，则代理fi中的进程tell（c）可以将c添加到其本地存储中。请注意，形式为tell（[c]fj（l）[d]fi（l′））、viarule（5）或fthestructuralcongruence的 过 程可 以 使 用 decom i来tell（[c]fj（ l ） ）tell（[d]fi（l′））以填充此规则中的边条件。• 如果一个代理fi愿意将原子公式A传送给另一个代理fj，它可以异步地发布约束fj（l）A。TDIS规则R说约束A被• 进程（localy;l）Q将局部变量y（resp.新的次指数变量l）到集合xi（分别为li）如规则RL所示（分别为RLL）。我们提醒您，左侧引入规则创建了新位置，并使其可供系统中的所有家庭使用（参见[18]）。然后，Rule RLL将l添加到系统中代理的所有配置中（参见示例3.7）。• 如果代理f i的本地存储di能够输入c [yJ/y][lJl]，则代理（abs y; l; c）Q演化为Q[yJ/y][lJ/l]并消耗约束c。请注意满足d►c[yJ/y][lJ/l]中的约束e不一定是唯一的。请为我们的安装实例!c1和!C（!c1）。在第一种情况下，我们有一个不受欢迎的削弱商店。为了避免这个问题，我们要求e是最一般的选择，如[9]所示。我们注意到代理f只能查询其自己的本地存储，因为guardc中的约束条件必须仅用f族的次指数来标记。• 规则RSTR指出，全等过程具有相同的约简。C. Olarte等人。理论计算机科学电子笔记305（2014）103115ǁ=f（out）。Σf（出）f（a）f（出）f（a）约束条件F=f（输出）f（b）f（a）c. 从序列F-开始→f（输出）f（a）c不是• 为了解释RS规则，考虑过程[tell（c）]l。我们从这个过程中观察到的是，约束[c]l被添加到了存储中。这意味着tell（c）的输出被定义为空间l。现在考虑过程[askcthenQ]l。在这种情况下，为了决定Q是否必须被执行，我们需要找出c可以做什么。 从位置l中的信息推导出。Hence，Rule R S的首映式只考虑了商店fi（l）di。 此外，该地点的新商店，即，该地点的新商店。dJi再次被放置在规则结论中所示的位置。• 规则RC只是简单地取消了进程名称p的定义。3.3在dccp在本节中，我们将展示一些可以在dccp中建模的分布式和并发行为的示例。我们还展示了本地和Abs程序的相互作用如何允许我们在代理商之间动态地创建共享和私有存储。当需要时，为了避免商店中没有任何次指数的配方，我们将...defsume，eachagent被定义为Agentf[P]Whereoutisabestexponetial标记代理商店中的"最外层例3.5[局部存储]设a和b为无界次指数，P=tell（c），Q =询问c然后告诉（d），R = [P] a[Q]b. 让代理f被定义为。DefA g=f=[R]或t。Hereweobservethefollowing：f：;;[R]out;1**f：[[Q]b]out;f（out）f（a）c/−→然后，Q仍然被阻塞，因为信息c只能在空间c中获得。A. 请注意，这是干燥的nt! f（出）？f（out）! f（a）？f（a）c−! f（出）？f（out）c不是provable，即信息c被定义为f中的内部空间a。现在让R= [P]a[Q]a。 然后，我们观察到作为最后一个存储的约束：CD这意味着Q可以在空间a中输入guardc，以便稍后将d添加到存储中。最后，considerR = [[P]a]b[Q]a。 在这种情况下，P最终会加上很可能，Q仍然被屏蔽。 这直观地意味着b所包含的空间到一个可能已经dideferently（即。（它包含来自a的自有空间的不同信息）。示例3.6[名称/链接移动性]名称移动性是通过考虑变量时abs和局部过程的相互作用获得的。假设实例化一个未解释的谓词符号com（·），让P=（localx）（tell（com（x）PJ）and116C. Olarte等人。理论计算机科学电子笔记305（2014）103。ΣQ=（absy;com（y））QJ和R=P如以下所示：Q. 然后是代理代理F。Def=[R]out贝哈维斯f：;;[R]out;1−→*f：

下载后可阅读完整内容，剩余1页未读，立即下载