多方交互的基于约束的语言及其在并发系统中的应用

可在www.sciencedirect.com在线获取理论计算机科学电子笔记351（2020）25-50www.elsevier.com/locate/entcs一种用于多方交互的基于约束的语言琳达Brodo2意大利萨萨里大学。Carlos Olarte3北里奥格兰德联邦大学摘要多方交互在当今的分布式系统中很常见。 探员通常会交流，在单个会话中，与其他代理一起完成给定的任务。以包括供应商、客户、信用卡系统和银行的在线交易为例。 当指定这种系统时，我们可能会观察到一个单一的交易，包括几个（二进制）通信，导致变化，所有相关探员的状态 多路同步过程演算，从一个二进制移动到多方同步纪律，已被提出来正式研究这些行为系统.然而，采用Bodei，Brodo和Bruni的核心网络代数（CNA）等模型可以从系统中观察到的状态/行为的数量在本文中，我们探讨机制来解决这个问题。我们扩展了CNA的约束，声明性地允许建模者限制实际应该发生的交互。我们的扩展进程代数，称为CCNA，在平衡并发系统中的交互中找到了应用，从而为并发系统中的哲学家的问题 我们对约束的定义是足够一般的，它排除了在多方谈判中积累成本的方法。因此，仅观察到关于建模者施加的阈值的计算。我们使用这种机制来巧妙地建模服务水平协议协议。我们开发的CCNA理论，包括其操作语义和行为等价，我们证明是一个同余。我们还提出了一个原型实现，使我们能够验证，自动，一些系统中探讨的文件。保留字：并发理论，约束，多方交互1引言目前，并发和移动系统在许多领域和应用中普遍存在。它们遍及科学的不同领域（生物和化学系统，1由于萨萨里大学的访问科学家赠款，作者的联合工作成为可能。Carlos Olarte也得到了CNPq的资助。Linda Brodo还获得了萨萨里大学的“fondo di Ateneo per la ricerca 2019”资助2电子邮件：brodo@uniss.it3电子邮件：carlos. gmail.comhttps://doi.org/10.1016/j.entcs.2020.08.0031571-0661/© 2020作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。26L. 布罗多角Olarte/理论计算机科学电子笔记351（2020）25τtems）、工程（安全协议和移动及面向服务的计算）甚至艺术（多媒体交互工具）。一般来说，并发系统表现出复杂的交互形式，不仅在其内部组件之间，而且与周围环境。因此，一个合理的挑战是提供计算模型，使我们能够理解这种复杂系统的性质和行为。作为对这一挑战的回答，进程代数，如CCS[17]，π-演算[18]和CSP[13]以及其他几个已经作为数学形式主义出现，以建模和推理并发系统。值得注意的是，没有统一的并发模型，就像顺序计算的λ事实上，并发是计算机科学中一个相对年轻的领域，有许多模型可以准确地捕捉某些行为，但忽略/抽象了其他一些行为。例如，CCS专注于进程的同步：通过展示互补的动作，两个进程握手并同步。然而，在代理之间实际上没有发送消息CCS的数据传递扩展允许克服这个问题，但是底层通信网络在计算期间保持不变，因为进程不能创建和通信新的/私有通信信道。π演算向前迈出了一步，允许名称（代表数据和通信链接）的通信，这些名称可以在以后的其他交互中使用。许多其他的过程代数已经成为现有过程代数的扩展，以处理特定的行为，或者它们从特定的系统中获得灵感，例如系统生物学的微积分。例如，Spi Calculus [1]将密码原语合并到π演算中，用于安全协议的指定和验证，而Brane Calculi[10]从细胞膜的相互作用中获得灵感，以模拟生物相互作用。所有这些形式主义的美丽依赖于它们的简单性（很少的运算符），形式语义和推理技术，包括行为等价性（例如，互模拟），模态逻辑和模型检查指定和验证系统文献中的大多数进程代数都集中在二元相互作用上。考虑例如CCS，其中进程a.P（P由输入动作a预先确定）可以与a.Q（Q由输出动作a预先确定）同步，当它们处于并行组合中在AP| a.Q）。这种同步通过一个特殊的作用τ（称为无声作用）来明确，我们观察到的是在过渡时期的这些进程|a.Q P和Q继续执行死刑。−→P|Q，在握手之后，在本文中，我们将专注于CCS的多方扩展，即所谓的核心网络代数（CNA）[4，6，5]，这是一种多方进程代数，其中每次同步的参与者数量不是先验固定的。在CNA中，CCS的二进制相互作用被扩展，并且通常的输入和输出前缀被推广到链路，例如， a\b，可以认为是将在信道a（输入信道）上接收到的消息转发到另一个信道b（输出信道）。CCS的标准输入和输出前缀在链接仅暴露输出（τ\b）或输入（a\τ）时被恢复;这些特定动作是链接链的末端，其中τ是无声动作（如CCS中）。链条是一种L. 布罗多角Olarte/理论计算机科学电子笔记351（2020）2527B在CNA中，n≥2个实体可以同步。每个实体必须拥有一个链接，该链接必须与另一个实体拥有的相邻链接相匹配。例如，如果三个进程分别对链路a\b、b\c和c\d进行同步，它们可以同步并产生链路a\b\c\d，其中信息从a通过b流到d，BCC.在[7，8]中，作者表明，CNA的多方和开放（任意数量的参与者）性质对验证的观点提出了有趣的问题。特别是，虽然CCS过程的可能后继状态的数量是其最外层前缀数量的二次函数，但在CNA过程中，它是指数函数。 此外，可以将一个主体图指定为一个CNA过程P（4.2节中的一些例子），并且我们可以检查图中是否存在一条哈密顿路径，如果P恰好有一个直接后继者。我们在[7，8]中探索了旨在驯服CNA转换系统固有复杂性的符号技术。本文的目标是定义一个合适的CNA扩展，允许规范以声明的方式控制进程的行为。更确切地说，我们提供了一些机制，允许我们在CNA规范中包含某些在手头的建模系统中自然出现的限制。例如，我们可能对图中具有特定长度的转换/路径感兴趣，或者指定开放交互中参与者数量的上限。这就是在前缀中引入约束和值的目的：过程a\b！vp（？P以给定的成本/值vp对链路a\b进行优化，并检查与其他进程的交互是否满足约束cp。当这个过程与，例如，b\c！vq（？cq）.Q，同步a\b\c具有最终成本v=vp+vq，并且如果v满足cp和cq，则实际上可以发生。正如我们将看到的，由于约束的控制机制具有有趣的性质，并且在定义这种扩展的过程中，我们找到了分布式问题的解决方案，这些问题在其他过程演算中没有简单的解决方案。 引用Jos'eMeseguer的话[16]，“增加表达能力不是理论上的奢侈，而是一个非常实际的目标，因为形式化的规范语言应该尽可能简单和自然地描述尽可能广泛的系统类。“.这正是我们的目标。捐款和组织。 我们从第二节开始回顾CNA的框架. 在第3节中，我们介绍了基于完备格和幺半群的约束的概念这样的结构允许我们比较值（例如，c42）并且还累积值（例如，将图中两条路径的长度/成本相加）。然后，我们扩展的语言CNA允许进程来传达这些值，并对它们进行查询约束。因此，只有当所有参与的代理人都满足自己的约束时，转换才能发生。我们称这种新的演算约束CNA（CCNA）。我们将证明CCNA是CNA的一个保守扩展（注3.7）：CNA过程可以看作是交换限制性较小的值并查询始终为真的约束的CCNA过程。在3.2节中，我们赋予CCNA一个合适的操作语义。这种语义与CNA的标准语义相比有一些新颖之处：我们采用了与早期方法相反的后期方法28L. 布罗多角Olarte/理论计算机科学电子笔记351（2020）25在[5]中使用。然后，我们的语义是固有的非确定性早期语义和[8]中的（更多涉及的）符号语义之间的一个很好的中间点。第3.3节介绍了CCNA过程的（网络）互模拟的概念，我们证明了这种等价是一个同余（从而允许我们在更大的系统中用等价替换等价）。在第4.1节中，我们展示了约束的使用导致了一个简单的解决方案，其中并发进程竞争使用一些资源的就餐哲学家问题。我们的解决方案是无死锁和公平的：所有代理都可以无限地进行。公平通常是作为一个外部条件强加的，但在这里，受约束的过渡制度满足了这样的要求。在第4.2节中，我们对一个代表交通系统的图进行建模，并展示了约束如何允许我们丢弃一些（不希望的）行为。此外，在第4.3节中，我们提出了一个应用程序的上下文中的服务水平协议（SLA）协议，约束自然表示限制，如上限的服务价格支付和最低质量（带宽）的客户端是期望。第五部分总结了本文的工作并介绍了相关的工作。我们还使用Maude系统实现了一个工具[16]。我们在这里不深入描述这种系统，但我们将在第5节中介绍它的使用。因此，我们贡献一个正式的框架，以指定约束多方互动和原型工具显示其适当的（自动）推理技术。2链接链相互作用设C为频道名称的集合，范围为a，b，c，. ，τ，Q是两个不属于C的不同符号。A = C <${τ}<${Q}是作用的集合，范围为α，β，. ，其中符号τ表示无声动作，而符号Q表示虚拟（非指定）动作。定义2.1（链接：实体，虚拟和有效）链接是一对l = α\β，其中α，β∈ A。 我们称α为l的源位点，β为l的靶位点。 A linkα\β是实的，如果α，β/= Q;链路Q\Q称为虚的。如果链接是实体链接或虚拟链接，则该链接有效。 我们将使用L来表示有效链接的集合。直观地说，a\b记录了一个动作a（或相当于通道a上的输入）和一个协同动作b（或b上的输出），这样a上的输入（从通信源接收）可以沿着通道b转发（到通信的目标）。当左边不需要相互作用时，使用τ-作用（如或右，或 链接τ\τ称为τ-link虚拟链接Q\Q表示稍后将完成的非指定交互。有效链路的示例是Q\Q、a\a、τ\a、b\a、τ\τ。链接Q\a、a\Q无效。链接可以组合在链接链中。直觉上，一个链环s = l1. L n表示多方交互，其中每个L i记录每个跳的源和目标站点。定义2.2（链环）链环是一个有限序列s = l1. l n个有效链接l i= αi\βi。我们说s是有效的，如果：L. 布罗多角Olarte/理论计算机科学电子笔记351（2020）2529β=τiQJ我βiB CQBBQ一BQτQ Q一BQB一 QQB一 B1β我(i) 对a lli∈[1，n），n∈βi，αi+1∈C 隐含βi=αi+1（ii）n ∈ [1，n]. I i/= Q\Q。;以及我们将使用VC来表示有效链环的集合。 链环的长度s（即， 以s为单位的链路数）将表示为|S|.条件（i）表示两个相邻的实体链接必须在其相邻的站点上匹配。为了突出这种匹配，我们将把链接链写为，例如，a\b\c\d而不是a\bb\cc\d中的链接序列。条件（i）还说，无声动作τ不能被虚拟动作Q匹配。正如我们将看到的，这是必需的，因为当过程在受限信道上同步时，τ-作用只能与τ匹配。 条件（ii）表示有效的链环必须至少一个实心链路（即，链Q\Q\Q是无效的）。一些有效链接链其中，Q\a\b\τ，a\Q\c\d和τ\a\τ。第一条链代表一种相互作用，在A\B的左侧存在未决同步;类似地，第二链表示第三方进程必须连接连接B和C的链路的交互（即，b\c）。最后，最后一个链是执行输出τ\a的进程和执行输入a\τ的进程之间的二元交互的结果。以下是无效链接链的示例：a\c\d、Q\τ\a和a\c\d。此后，我们只考虑有效链接和有效链接链。我们将使用“无效”来表示无效的链接和链。现在我们引入合并运算符s·sJ，它作用于两个相同长度的链环，即|S|为|SJ|.直觉上 ， s·SJ 使 两 个 链 接 链 折 叠 成 一 个 链 接 链 ， 其 中 s （ resp.s ） 已 被 替 换 为 sJ（resp.s）。定义2.3（合并）设α，β ∈ A为作用。操作上的合并运算符定义如下：如果β=Q，则α·β=α如果α=Q，则α ·β=β否则对于链路，设l1=α1\β，l2=α2\βα1·α2= x α，β1·β2= x β。如果x α，x β≠ 0，则l1·l2 = xα|x。否则，l1·l2 = l。对于合并在链上，让s = l1. l n和sJ= lJ1. lJn是满足l i= αi\β的有效链，lJi=α′i\β′。如果对所有i∈ [1，n]，li·lj i / = n，且（l1·LJ1）. （l n·lJn）是有效链，则s·sJ=（l1·lJ1）. （l n·lJn）。否则，s·sJ= 0。例如，链Q\Q\a\b和c\Q\Q不能合并，因为它们具有长度不同;a\Q\Q和Q\c\d无法合并，因为a\c\d不是有效的链; a链s不能与自身合并;最终，c\Q\b\d和Q\a\Q\Q合并为c\a\b\d。在进程演算中，名字通常是受限制的，以便强制交互。设s = l1. l n=.αi\αi+1\βi+1. 是一个链接链。 我们说a在s中匹配如果两(1) ai=α1和ai=βn（即，a不能发生在端点中），并且230L. 布罗多角Olarte/理论计算机科学电子笔记351（2020）25⎨否则，一 B一 Q一 BτB(2) 对任意i∈[1，n），βi=αi+1=a或βi，αi+1/=a.否则，我们说a在s中不匹配（或待定）。 例如，a和b在τ\a\b\d中匹配。 相反，a和b在d\Q\c\b中都不匹配。定义2.4（限制）设α，β∈ A为动作，a∈ C为通道名。我们定义了以下关于操作和链接的操作（ν a）α=πτ如果α=a否则，和（ν a）α\β=（（ν a）α）\（（ν a）β）我们将这些操作提升到以下链接链：（νa）s=（（νa）l1）. . . （（νa）ln）如果a在s中是match例如，在s=τ\a\Q\Q中，名称a匹配，并且（νa）s=τ\τ\Q\Q;而（v b）s是unfined，因为b在s中待定。3带约束的CNA在本节中，我们将介绍配备了数据传递和对这些数据的约束的CNA演算。与链接演算[5]（以及在这方面的π演算）不同，我们将考虑不是通道名称的值，因此它们将有一个单独的定义集。我们的目标是对交互中的参与者可以共享的数据执行一些检查。值将从一个代数结构中获取，该结构允许我们比较（≤）并累积（≤）这些值。下面的定义来自[11]，在某种程度上简化了c-半环[3]的表示（另一种用于累积和比较约束的代数结构）。回想一下，偏序是一个对<$D，≤ <$，使得D是一个集合，≤是D上的自反、传递和反对称关系。我们用表示的严格版本≤（即，如果v≤vJ且v vJ，则v≠ v j）。我们也使用≥和>与预期的意义。一个完备格是一个偏序，其中任何子集X<$D都有一个最小上界表示为HX。通过对偶，最大下界，记为HX，也存在。像往常一样，我们用T和H分别表示HD和HH。交换幺半群是一个三重幺半群D，T，其中T：D × D → D是一个交换和结合算子，T是它的单位元（即，v∈ D.v<$T=T <$v=v）。定义3.1（CLM [11]）一个完备格幺半群（简称CLM）是一个元组K = D，≤，s. t。是一个完备格，T和T分别是D的最小和最大元素，并且是一个交换幺半群。 我们假设，在glb的分布， 即 ，Dv ∈ D. X| x∈X}L. 布罗多角Olarte/理论计算机科学电子笔记351（2020）2531让我们用一个具体的例子来解释上面的定义，我们将在下面的章节中使用这个例子。考虑结构KN=<$N∞+，≥，+<$其中N∞+是由∞完成的自然数集合，≥是N ∞ +上通常的 5≥2）。 我们可以把N∞+中的元素看作是成本。 注意，我们将0视为“最佳”（T）c=t（x≤0，即， x≥0，nyx∈N∞+）。此外，∞是我们可以假设的最坏（最坏我们用+（N上的加法）来累计成本。当成本增加时，我们得到“更差的成本”（例如，3 + 2≥3）。更一般地说，我们可以证明，n是一个密集算子：nv，vJ∈ D，v<$vJ≤v。还可以证明，对于λ，λ是吸收的（即，v∈ D.v<$$>=<$）。 在我们的具体例子中，v+∞=∞。定义3.2（留数）设K = φ D，≤，φ j是一个CLM，v，vJ∈ D。v关于vJ的剩余定义为v <$vJ= H{x ∈ D |v ≤ vJ<$x}。正如预期的那样，v≤vJ<$（v<$vJ）（由于分布性）。此外，如果vJ≤v，则v<$vJ=T。InKN，n是nN∞+的减法 （v<$vJ=v−vJ）ifv≥vJ（即，v≤ vJ），否则为0。（参见[2]关于基于约束的形式主义中剩余的讨论可以组合不同的CLM，以便在单个操作中测量/比较不同的实体。引理3.3（组合CLM）设K1=<$D1，≤1，<$1 <$$>和K2=<$D2，≤2，<$2<$是CLM.定义K = K1×K2 =<$D1×D2，n，n其中（v，w）≤（vJ，wJ）i <$v ≤1vJ且w≤2wJ;且（v，w）n <$（vJ，wJ）=（v <$1vJ，w <$2wJ）. K是一个CLM。证据任意lubs的存在是K1和K2中存在lubs的一个简单推论。分配也很容易。注意，我们也可以在K上定义（逐点）剩余。Q3.1受约束的多方交互现在我们准备好介绍约束CNA的语法，从现在开始表示为CCNA，它相对于CLM是参数化的。在下文中，我们用剩余算子k来固定CLM K = k D，≤，k。我们将用u，v对D中的元素进行值域.我们将把数据变量称为变量（通常表示为x，y，.）。），从D中取值。定义3.4（CCNA的语法）给定一组通道名称C（由a，b组成）和一个CLMK，CCNA中的进程根据以下语法构建：exp * = a | v| X| 经验值 | expexp表达式atm：：=exp*expJ，其中*∈ {≤，n，=，，≥，>}原子约束c，cJ ：：= atm| c→c →J约束p，q* = 0| 我知道！e（？c）.P| p+q序列过程P，Q：：= p| P|Q| （ν a）P| 一个1，...，a n; e1，...， 电磁 过程32L. 布罗多角Olarte/理论计算机科学电子笔记351（2020）25其中a是表示交互作用的累积值的可区分的数据变量;v∈ D;x是数据变量;e是a不出现的表达式;l = α\β是从C { τ }构建的实体链接（即，a，βQ）;A是一个过程标识符，我们假设A（b ; x）P形式的（可能是递归的）定义，其中b是成对不同名称的列表，x是成对不同数据变量的列表;e i是a不出现的表达式。Q在以下段落中，我们将详细解释该定义的各个组成部分。符号a表示累积（使用）的特殊数据变量（3）每个参与者在互动中增加的价值（定义3.10在KN中，有效表达式的例子有3、5−y、5 +x+a等。约束将用于检查代理是否同意给定交互的值。在KN中，原子约束的例子是5≥3，x≥4，x≥y+ 3，a≥10等。约束就是这些原子的结合我们用tt来表示（总是为真的）原子约束条件T ≤ T。在解释过程的意义之前，我们需要一个额外的定义。（数据）变量的唯一约束是过程定义A（b;x）P，其中x中的变量在P中发生约束。我们将使用fv（P）来表示自由（数据-）过程P中的变量。我们还将使用fv（c）来表示自由（数据-）的集合。c中的变量（包括a）。定义3.5（蕴涵）我们说约束c是基础，如果它不包含数据变量，也不包含符号a（即，fv（c）= 0）。给定一个基本原子约束c = e * eJ，我们说c成立，记为K|= c，如果e和eJ分别约简（在K中执行运算和）为v和vJ，并且关系v * vJ在K中成立。否则，我们写K| = c。我们将这个概念扩展到地面约束，如下所示：|=c1<$· ·<$c n，当K| = c ifor alli∈ 1.. n.设c，c， J是约束s. t。fv（c），fv（cJ）<${a}. 我们说c， CJ是等价的，记为c<$cj，如果<$v∈ D. K| = c [v/a] iK| = cJ[v/a]。例如，我们有以下蕴涵：|= 3 + 2 ≤ 1 + 2 ;且KN|= 3 <$2 ≥ 1 + 2。此外，如果c1=tt<$3≤a且c2=a+ 0≥ 5<$2，则c1<$c2。进程0不执行任何操作。这个过程很简单！e（？c）.P将实体链接l连同由表达式e表示的值一起进行运算，并检查约束c是否成立。在这种相互作用之后，过程表现为P。非确定性过程p+q可以表现为p或q。 交织并行合成表示为P|Q.过程（ν a）P表现为P，但它不能表现任何作用量a。 因此，我们可以说a在P中是局部的（或私有的）。通常，（ν a）P约束a在P中的自由出现。的呼叫一个1，...，a n; e1，...，e m表现作为的进程P[a1/b1，.，a n/b n][e1/x1，.，e m/x m] 如果 的 恒定一是已定义作为A（b1，...，b n; x1，.，x m）P.正如所预料的那样， 实际参数代替了定义的形式参数。除了绑定变量x i之外，above定义还绑定了名称bi。We应使用fn（P）和dbn（P）分别表示P中的自由名和束缚名。L. 布罗多角Olarte/理论计算机科学电子笔记351（2020）2533BQDQB C我们将对文学中常见的过程施加一些限制（例如，[12]）。定义3.6（有效进程）进程被带到alpha转换（重命名绑定名称）。我们假设在过程定义A（b; x）P中，fn（P）<$b和fv（P）<$x。此外，为了保证转移系统是无限分支的，我们假设P中的递归调用必须在一个前缀l中被保护！e（？c）Q.最后，我们假设在所有过程中，数据变量x（不同于a）的出现总是受到过程定义的约束。例如，进程l！2（？x>5）.Q和l！2+x（？a>5）.Q是无效的，因为x是自由的（并且不受过程定义的约束且工艺def定义A（）= A|P是无效的，因为调用A没有被保护（因此使得（transition system in finitely branching）。3.7为了便于阅读，我们将使用以下快捷方式。我们将省略尾随的0，例如。用\b代替\b0。 我们也要写L！是我，是你！e（？tt）。 回想一下，对于所有v∈D，v <$T = v。因此，我们可以写l（？c）而不是l！T（？（c）。最后，我们将简单地写l而不是l！T（？tt）。注意，任何CNA过程也是CCNA过程，其共享值（T）与最终交互无关，并且其约束始终保持（tt）。下面的示例说明如何使用约束来限制多方交互中的参与者数量。目前，关于进程行为的讨论仍然是非正式的，直到我们在下一节定义语义。例3.8进程P= a\b能够与任何其他进程相互作用，比如Q = c\d，并同步产生链环a\Q\c\d。 其他产出也可以从这种相互作用中预期，例如，c\Q\a\b。 事实上，一个三方与另一个进程R= b\c同步也是可能的，从而构建链a\b\c\d。 更一般地说，P可以与无限数量的其他通过构建合适的（有效的）链接链来处理。这意味着CNA中的交互是开放的，因为参与者的数量不是先验固定的。这是微积分的一个非常有表现力的特征，但它也使推理过程变得困难(See[7]和[8]的符号技术来处理这个问题）。考虑结构K N和下面的过程PJ=a\b！1（？a≤2）QJ=c\d！1（？a≤2）RJ=b\c！1（？a≤2）因此，PJ最多只能与其他两个过程（Q j或R j）中的一个相互作用，因为在每次相互作用中，值1被累加，并且该值必须小于2。这是一种非常直观（和声明性）的机制，用于计算和限制交互中的参与者。Q派生构造（元组）。让我们介绍一个有用的惯用结构。由于引理3.3，我们可以假设代理人与元组的链接，34L. 布罗多角Olarte/理论计算机科学电子笔记351（2020）25−→−−−−−→−→−→−−−→μμμμ法pμPJ勒苏姆q−→QJ的简历我知道！e（？c）.Pl！e（？c）Pp+q−→PJp+q−→QJμJQμQJPμPJQφQJLPAR−→Rpar−→−→ComμP|Q −→ PJ|QμP|Q −→P|QJP|Qμ·φPJ|QJμP[a/b][v/x]−→PJA（b;x）PIDEPμPJResAa;vP −→PJ（νa）P（νa）μ（νa）PJ图1.一、语义所有规则都有一个附带条件，即转换中的标签是有效的（定义3.10）。元件，例如， （e1，.， e n）。这样的元组是CLMK1×···× Kn的元素。因此，我们将使用更方便的符号我知道！e1，.，e n（？c1···cn）其中，每个约束Ci可以使用特殊符号Ai（表示元组的第i个 注意，这些元组和约束可以通过使用引理3.3中的结构很容易地用定义3.4的语法重写。由于每个CLMKi表示要计算的不同值/测量，因此在相同表达式中组合不同CLM的值是不合法的。例如，表达式，例如，a1a2不合法。约束也是如此。下一个符号约定允许我们为“累积”变量a i提供别名符号3.9（元组和变量）对于给定的规范，我们可以确定交互中使用的元组的形式为1，...，其中别名x i不能约束通过一过程定义。所 以 ，我们写L！x1= e1，.，x n= e n（？c1 · · · ∧ cn）到我的意思是！e1，.，e n（？（c1··cn）[a1/x1，.，an/x n]）。此外，如果v i= T，我们进一步省略“x i = T“。比如说，如果我们确定元组形式为：成本，速度，表达式l，speed= 1（？成本≤3倍速度≥ 10）意味着l倍！T，1（？a1≤ 3 ≤a2≥ 10）。3.2语义在本节中，我们将介绍CCNA的操作语义。这种语义的新颖之处在于使用了后期方法，其中仅在通信规则中推断参与者的数量，而不是[4]中采用的早期方法（其中规则Act需要“猜测”交互的大小）。这一区别将被简单地阐明。在定义语义之前，我们将提升链接链上合并的定义（定义2.3），以便也考虑形式为s的值约束链（VCC）！e（？c）其中s是链接链，e是基础表达式（无自由变量），并且 c是一个约束，其中fv（c）≠ {a}。为此，我们允许链接链被放大（注入虚拟链接），或者通过关系式（定义如下）收缩。L. 布罗多角Olarte/理论计算机科学电子笔记351（2020）2535Q−→一一 Q定义3.10（值约束链和运算）我们设（是在公理下闭的链环上的最小等价关系（只要两边都是有效链环）：sQ\Q（s s1Q\Q\Qs2（s1Q\Qs2Q\Qs（s s1α\a\βs2（s1α\Q\a\βs2我们合并VCC如下：s！e（？c）·sj！eJ（？cJ）=（w·wJ）！eeJ（？c<$cJ），其中s<$（w）和sJ<$（wJ）。我们定义（νa）（s！e（？c））as（（νa）s）！e（？（c）。我们说，一个VCCs！e（？c）是有效的，i s是有效 的链环，并且K |= c [e/a]。我们将使用μ、φ来对VCC进行测距。请注意，这些值是使用CLM中的“”运算符合并的。还要注意，为了检查VCC的有效性，符号a被替换为当前累加值e。由于我们假设在一个过程中没有自由的数据变量（见定义3.6），一旦定义的数据变量被具体的值所取代，c[e/a]确实是一个基础约束。最后，由于在值和约束中没有出现名称，VCC上的限制操作只作用于链环（定义2.4），因此e和c保持不变。结构操作语义由标记转移系统（P，VCC，−→）给出，其中状态集P是CCNA过程的集合，标签是有效的值约束链（VCC），转移关系−→是由图1中的规则生成的最小转移关系。Prefix进程是！e（？c）.P简单地将链接l与值/表达式e连接起来并检查C是否有效，即，我知道！e（？（c）必须是有效的VCC（规则法案）。如果p能够表现出到PJ的跃迁，标记为μ，然后p+qμPJ（规则Lsum）。q（RuleRsum）。如果P可以呈现转换，则当与Q并行运行时，它也可以呈现相同的转换（规则Lpar和Rpar）。 在保留地，如果P使动作μ成立，则（νa）P使（νa）μ成立（如果它成立）。规则Ide简单地用实际参数替换形式参数同步机制（RuleCom）通过合并两个VCC来工作在这样做时，请注意，链环可以被放大（定义3.10），因此，一个链条的链环可以被放置在另一个链条的容许位置。注意，关于结果链的长度的决定被推迟到使用规则Com。这是一个不同的方法从一个考虑在[4]（对于CNA过程），其中相互作用的大小必须在Actrule（通过在本规则中使用（）扩大l我们还注意到，与CCS相反，CCNA（和CNA）中的规则Com可以在转换的证明树中出现多次，因为合并操作符总是可以注入更多的虚拟链接以允许其他代理参与，如以下示例所示例3.11考虑CLMKN和过程：P=τ\a！2（？a≤10）.PJQ=a\b！3（？a≤12）.QJR=b\τ！5（？a≥4）.RJ36L. 布罗多角Olarte/理论计算机科学电子笔记351（2020）25a B\ \ \ （啊！10分（？a≤10a≤12a≥4）τττ^^^ ^您的位置：S1S2S31Snσσ一 Bττ一例3.12（条件）给定原子常数c=e1*e2，let^cBQ\b（！3（？a≤12）法Q′R\τ（！5（？a≥4）法R′法−−−−−−−−−−−→−−−−−−−−−−→网\a（！2（？a ≤ 10）′\\τ（！8（？a ≤ 12a ≥ 4）′′BP−→PQ|R−−→Q|Rτa b网P|Q|R\a\b\τ（！10分（？c）、P′|Q′|R′（νa，b）（P|Q|右）−−−−−−−−−−−−→τ τ τ−−−−−−−−−−−−−−−−−−−−−−−→ （νa，b）（P′|Q′|R′）2×分辨率图二. 例3.11中的推导。代表三个对建房子感兴趣的经纪人他们每个人都有她的服务成本（例如， P收费2美元）。 此外，P不愿意参与成本超过10美元的项目，R不参与成本低于4美元的“小”项目。P需要有人提供与其输出链接a匹配的服务。 Q表示a并期望交换b，R提供b。 这三个智能体确实可以参与项目，如图3.2所示。 注意，（νa，b）τ\a\b\τ= τ\τ\τ。此外，在该推导的所有步骤中，转换是有效的VCC。在推导过程中使用了两次RuleCom，因此产生了三方交互。如果我们把P2定义为τ\a！2（？a10）.P2J< 过程（νa，b）（P2|Q|R）不有任何过渡以来，S！10分（？a<10 mA ≤ 12 mA ≥ 4）不是有效的VCC。此外，名称a，b是受限制的，P2中没有任何进程|Q|R可以使用规则Lpar和Rpar（例如， a在τ \ a中不匹配，则（νa）τ\a无效）。换句话说，P2拒绝与Q和R进行三方交互，因为项目的成本将超过她的 预期。Q表示原子常数e1^*e2，其中e^*用=，≤用>，≺对于≥，等显而易见：(1) C=c;以及（2）给定基原子约束c，K| =ciK |= c。 我们可以定义一个条件结构，根据约束的蕴含来选择过程的继续。更准确地说，如果c = c1<$· ·<$cn ，其中每个c i都是一个原子约束，我们可以写l<$！e（if？cthenPelseQ）表示过程l！e（？c）.P+l！e（？c1）.Q+···+l！e（？c n）。请注意，只要所有c i成立（因此c成立），就执行P，如果有一个c i不成立，则执行Q。潜在的CLMQ定义3.13（计算）设W是有效VCC的有限和无限序列的集合。 设P是一个过程，σ = s1，s2... ∈ W ≠无穷大顺序如果P = P0−→P1−→P2−→· · ·，我们说σ是P的计算。如果P不能为任何跃迁的幂次，我们就写P-→，称P为死锁。如果σ=s1，s2... sn∈sWn是有限的s equen ce，我们说σ是（有限）计算如果P= P0−→P1···Pn−1 −→P n−→。 在这两种情况下，我们都记为P-→。我们将使用O（P）<$W<$来表示集合{σ|P −→}。τL. 布罗多角Olarte/理论计算机科学电子笔记351（2020）2537α τμ−→−→3.3网络互模拟现在我们定义一个CCNA过程的行为等价，我们证明它是一个一致性。在CNA的传统中，我们不区分表现出不同内部过渡的过程。这反映在[4]中最初提出的等价关系DD的以下扩展中。定义3.14（等价DD）我们让DD是在以下推理规则下闭合的链接链s（sJsDDsJs1\τ\β s2DDs1βs2我们解除这样的关系，VCC如下：s！e（？c）DDsj！e（？cJ）i=DDsJ，以及ccJ.定义3.15（网络互模拟）网络互模拟R是CCNA过程上的二元关系，如果PRQ，则：μ• 如果P−→• 如果Q−→PJ，则φ，QJ使得μDDφ，QφQJ，则φ，PJ使得μDDφ，PφQJ和P JRQJ;P j和P JR QJ。P和Q是网络双相似的，记作P<$Q，如果存在网络互模拟R s.t. P R Q。遵循标准技术（参见例如，[12，23]），我们可以证明，它是一个等价关系，它是最大的网络互模拟关系。让我们用结构KN给出一些说明性的例子。对于任何P，0l！3（？a≤ 2）.P，因为KN/|= 3 ≤ 2。 此外，合并约束不能使a≤2有效（由于a的密集性）。 ≤，即，a总是大于3）。过程P=l！3（？a≤5）和Q=1！3（？a≤7）不能被认为是等价的：例如，Q可以与R=lj同步！4、P不能。现在考虑P=l！2（？a≤2）且Q=l！4（？a≤4）。注意，两个进程都可以与形式为R=lj的进程同步！0（？（c）。然而，如果c=a≤ 2，P和R可以同步，但Q和R不能。接下来，我们证明了“equals”是一个同余关系，然后，我们可以在任何上下文中替换“equals”。为此，让C[·]表示一个只出现一次孔[·]的过程表达式。此外，如果P是一个过程，则C[P]表示用P替换空穴[·]而得到的过程表达式。定理3.16（同余）如果P <$Q，则对任何上下文C [·]，C [P]<$C [Q]。上述定理通过展示任何情况/上下文的适当网络互模拟来证明。完整的证明在附录中4应用：公平性和受约束的交互在本节中，我们将给出三个引人注目的示例，展示如何通过约束以声明方式控制多方交互第一个例子是α38L. 布罗多角Olarte/理论计算机科学电子笔记351（2020）25S1S2S3n吃饭的哲学家的典型问题。在这种情况下，通过添加约束，我们能够为问题指定一个无死锁且公平的解决方案。第二个例子模拟了一个网络运输系统，其中约束可以表示成本或时间限制。在我们的最后一个例子中，约束用于在协商协议中对服务级别协议4.1吃饭的哲学家以用餐哲学家（DP）为例，研究了共享资源的并发实体之间的交互。这个问题涉及到n个哲学家围坐在一张桌子旁，每个人都有自己的菜，他们只能吃或思考。当他们独立决定吃东西时，他们需要两把叉子。在桌子上，两个盘子之间只有一个叉子，即，n个叉子。众所周知，仅使用二元交互[12]的系统没有对称和无死锁的规范，例如，CCS。让我们只考虑两个哲学家来说明这个问题。哲学家被称为CCS过程Pi=fi.f（i+1）mod2.eati.PiJ其中P0首先抓住叉子0，然后他拿着叉子1稍后开始吃（类似于P1）。如果我们并行运行P0和P1以及指定两个fork的进程（Fi= fi. FiJ），当P0取fork 0而P1取fork 1时，系统可能会陷入死锁。通过使用多方同步演算，DP问题具有简单且非常自然的无死锁规范（参见[7，8]使用CNA和[12] 使用Multi-CCS的解决方案）。在这种情况下，在原子（或多方）交互中，哲学家同时使用两个分叉，从而避免了上述死锁情况。然而，多CCS和CNA中的解决方案可能表现出不公平的计算，例如，某个哲学家总是在吃或在想（其他人则无法进步）。定义4.1（Fairness[24]）Le π是一个无限次计算，π=P0 −→P1−→P2−→· · ·。 VCCμ在π中被无情地使能，如果πJJ，πJs. t。 π=πJJπJ，πJ包含一个过程P i，它可以对一个标记为μ的跃迁进行排序。此外，如果π j上的每个无情地使能的VCC μ发生在π j中，则π是强公平的。换句话说，如果在π中不断启用的动作（VCC）在π中无限频繁地发生，