简单进程代数的Petri网语义

理论计算机科学电子笔记154（2006）71-94www.elsevier.com/locate/entcs一种简单进程代数的Petri网语义Raymond Devillers1D'epartemmentd汉娜Klaudel2LaMIUMR8042CNRS，Universit′eEv ry-ValdMaciej Koutny3纽卡斯尔大学计算机科学学院Newcastle upon Tyne，NE17RU，United Kingdom摘要在本文中，我们提出了一个结构性的翻译条款从一个简单的变种的KLAIM进程代数到行为等价的有限高级Petri网。这就产生了一个正式的语义的流动性，允许一个直接处理并发性和因果关系。关键词：移动性，进程代数，KLAIM，Petri网，组合翻译，行为一致性。1引言计算机技术的理论和应用中增长最快的领域之一是网络感知计算，它支持新的编程语言和理论，这些语言和理论通过分布式系统内的基本交互机制来利用代码移动性。在用于处理结果系统的复杂性的方法中，除了例如π演算所使用的同步通信范例之外，基于LINDA[11]的那些方法发挥了突出的作用，1电子邮件：rdevil@ulb.ac.be2电子邮件：klaudel@lami.univ-evry.fr3电子邮件：maciej. newcastle.ac.uk1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.05.00872R. Devillers等人理论计算机科学电子笔记154（2006）71位置0位置1位置2位置0位置1位置2第一阶段：位置0位置1位置2第二阶段：位置0位置1位置2第三阶段：位置0位置1位置2第四阶段：位置0位置1位置2第五阶段：位置0位置1位置2第六阶段：位置0位置1位置2第八阶段：图1. 简单移动机器人示例的初始执行序列扩展了分布在网络节点上的多元组数据空间。在本文中，我们关注的是KLAIM（Kernel Language for Agents Interaction and Mobility），这是一个实验性的琳达启发的项目，包括各种移动计算的编程语言[3]。它包括一组协调原语（特别是，那些需要支持异步消息传递），一组操作符，用于构建过程中采取的进程代数和一些结构的顺序编程。KLAIM区别于更标准的编程框架的方式是它支持显式位置，这是可以由活动进程操纵的第一类数据，以及位于网络位置的进程之间的受控交互为了介绍本文中使用的移动性范例的基本概念，我们将使用图1所示的简单移动机器人运行示例（SMR）。机器人在由三个不同的明确命名的位置组成的网络中运行：0，1和2。每个位置都拥有自己的本地存储空间，称为元组空间，它可以保存由（迁移）进程存放和删除的数据元组。在起动器SMR⟨1 ⟩⟨2 ⟩⟨0 ⟩⟨1 ⟩SMR0⟨2 ⟩⟨0 ⟩⟨1 ⟩SMR0⟨0 ⟩⟨1 ⟩SMR0⟨0 ⟩⟨0 ⟩⟨1 ⟩⟨0 ⟩SMR1⟨0 ⟩⟨1 ⟩⟨0 ⟩SMR1⟨1 ⟩⟨0 ⟩SMR1⟨1 ⟩SMR2⟨1 ⟩⟨0 ⟩⟨1 ⟩R. Devillers等人理论计算机科学电子笔记154（2006）7173在我们的例子中，我们假设每个这样的元组是单例局部4;例如，在阶段1中，局部0的元组空间包含一个包含局部1的名称的元组1，而在阶段3中，局部2的元组空间是空的。 在我们的示例中只有一个进程SMR，它被描绘为在网络中移动的阴影正方形（最初，在阶段1中，位置0的启动器将机器人部署在位置1）。除了是移动的之外，SMR还保持其自己的私有数据-网络位置（最初，该数据等于0，即，起始位置）。机器人的预期行为可以理解如下：SMR希望通过从其当前位置的元组空间拾取元组来发现下一步移动的位置，并且在移动到那里之前，它输出其私有数据作为新的元组，并通过存储当前节点的位置来直观地说，这可以看作是一个无限循环：永远做输入 地点使用输出先前存储的位置存储当前位置移动到使用在图1中，我们展示了系统在第一阶段初始化后可以经历的八个连续阶段。由于每个位置在开始时只包含一个元组，因此整个系统是确定性的和非终止的。数据越多，行为就越不确定;数据越少，行为就越终止。移动应用程序的复杂性不断增加，这意味着对它们的有效分析和验证的需求现在是至关重要的。本文旨在解决这一需求，使技术和工具开发的Petri网理论，特别是那些基于明确的因果关系和并发性，可访问的移动计算系统的开发人员。更具体地说，我们将集中在一个语义保持翻译从一个基本的KLAIM启发进程代数高级Petri网。翻译是为来自TOY KLAIM的过程术语设计的，T oy K laim基本上是CKLAIM[3]的扩展，具有来自STOCK KLAIM[8]的一些特征。这产生，通过标准的Petri网理论，一个正式的语义的流动性，允许一个直接处理并发性和因果关系。新的表示法也应该是有用的自动验证行为属性使用合适的模型检查技术和工具。本文件的结构如下。我们首先描述语法，语义我叫你。之后，我们介绍了我们的翻译TOY K称之为Petri网，这是随后的翻译本身我们还建立了行为等价的Petri网模型和原来的TOYKLAIM表达式（所有的证明正式结果的附录中）。我们假设读者熟悉高级Petri的基本概念4.我们有意使进程之间交换的数据保持简单，以便集中于流动性方面建模所涉及的关键问题。74R. Devillers等人理论计算机科学电子笔记154（2006）71（COM）N1N2N1N2（A SANS）（N1<$N2）<$N3<$N1<$（N2<$N3）（A BS）l：：P<$l：：（P|无）（P RI）l：：A（n1，. ...，nmA/umA} PA（C LONE）l：：（P1|P2）l：：P1l：：P2表1结构等同性。网;然而，我们将提供足够的直觉，使文件访问那些不是真正的专家在这一领域。2的杜克莱姆进程代数我们首先给出了TOY KLAIM的语法和语义，它基本上是CKLAIM[3]的扩展，具有从STOCK KLAIM[8]中提取的一些特征（如非确定性选择）我们假设L是由l，LJ，l1，. 并且U是由u，v，w，uJ，vJ，wJ，u1，v1，w1，.他们的工会，连同杰出的地方自我，形成了一套名称N范围内的n，nJ，n0，n1，.。. ;也就是说， N= L U {self}。 此外，A ={A1，.，AK}是进程标识符的有限集合，每个标识符A ∈ A具有元数mA≥ 0。玩具KLAIM的定义流程和模板：分为四个部分，即网络，5个行动，N：：= l：：Pı l：：lNa：：= out（n）@ n_newloc（u）_inin（t）@ n_eval（A（n1，.，nmA））@ n（动作）P ：：= nilA（n1，.，nmA） 你好PP+PCUP |P（过程）不：：=n！u（模板）此外，对于每个进程标识符A∈ A，全局上只有一个可用的进程标识符。DF形式A（u1，.，umA）=PA，其中uiuj对于ij。结构性等价网络是最小的同余，使得网络中的等式表1保持（注意，{n1/u1，. ，nmA/umA}表示取代）。网络. 这些是本地化数据和流程的有限（由于规则COM和ASIGN）集合。可以将网络看作是唯一命名的地点的集合，每个地点包括其自己的数据空间和/或在那里运行的（并发）进程（参见CLONE规则）。[5] KLAIM中使用的原始术语是R. Devillers等人理论计算机科学电子笔记154（2006）7175行动这些是由进程执行的基本（原子）操作：（i）out（nJ）@ n将由nJ表示的位置的新副本存放在由n寻址的位置内;（ii）in（t）@ n从位置n检索与模板t匹配的项;（iii）eval（A（n1，.，nmA））@ n在局部n中启动由A标识的进程的新实例;以及（iv）newloc（u）创建新的网络局部（具有nil进程），其地址使用局部传递到系统变量u请注意，特殊的局部性self的特殊含义是，它指的是执行动作的局部性地址。还要注意，在任意位置实例化一个进程允许对移动性进行流程. 这些是唯一的计算单元，作用于存储在不同位置的数据，创建新的位置并产生新的过程。进程的代数是建立在（终止的）进程nil和三个复合运算符之上的：通过一个动作（a）进行前缀化。P）、选择（P1 + P2）和平行组合（P1|P2）。约束力和良好的形式。prefixes newloc（u）. P和in（！u）@ n. P（即，位置创建和输入）将局部变量u绑定在P内，然后我们用fv（P）表示P的自由变量（对于网络也是如此）。注意到变量（如果在过程定义中多次使用）可以有自由和（可能很多）绑定的出现。例如，u在（！u）@ u。nil是绑定的，而第二个是自由的。像往常一样，过程被定义到alpha转换，这意味着绑定变量可以被一致地重命名，以避免潜在的冲突。此外，委员会认为，{n/u，. } P通过用n替换u的所有自由出现等从P获得，可能在α转换P之后，以避免冲突;例如，{l/vJ，u/uJ}in（！u）@ vJ. out（u）@ w. A（uJ）= in（！uJJ）@ l. out（uJJ）@ w. A（u）.注意，self是一个局部变量，而不是一个变量，因此它永远不会是自由的。 对于如上所述的过程定义，我们假设fv（PA）={u1，.，umA}，使得PA的自由变量实际上是参数有界的。给定一个网络N，可以应用alpha转换以获得一个良好的网络定义。我们的意思是，在网络和过程定义中，没有一个变量既自由又有约束，也没有一个变量产生一个以上的约束。此外，我们假设网络中没有自由变量（变量u只有在它发生在（！u）或newloc（u），或作为形式参数）。因为-stance，l：：in（！u）@ u。out（self）@ lJ. 零，l ：：out（u）@ self。in（！u）@ self。nil和l：：in（！u）@ self。in（！u）@ l. nil不是良构网络，因为在前两个网络中，u既受约束又自由，而在第三个网络中，u受两次约束递归行为可以至少以两种不同的方式实现。一个是流程实例化（这将被称为“显式创建”），可能在当前位置。例如，l：：eval（A（lJ，lJJ））@ self。nilwithA（u，v）=dfout（v）@u. e va l（A（u，v））@self. 无76R. Devillers等人理论计算机科学电子笔记154（2006）71−−−→−−−→−−−→−−−→−−−−→（PAR）法LN−−→莲莲JJ法林贞贞法法LJNJLJNjNJJLjNJJNJLJNJ（SUM1）−−−−→Ll：：P+PJactLl：：PJ+PactLJNJLJNJLl：：PlJ：：lJJ法⟩−−−→ LJNJ（SUM2）Ll：：P+PJlJ：：ljjactLJNJLl：：PJ+PlJ：：lJJ法⟩−−−−→ LJNJ（S结构）N N1莲法1−−−→ LJN2N2NJ法LN−−→LJNJ表2操作语义规则将从具有地址l的位置无限期地将位置l_J的副本存放到由l_j寻址的位置的数据空间。然而，这种定义的一个副作用是动作eval（A（lJ，lJJ））@self也将被执行并记录在操作语义中。这可能是可取的，也可能是不可取的，因此我们有另一种方法来通过声明l：：AJ（lJ，lJJ）来验证递归行为（总是在当前位置），AJ（u，v）=dfout（v）@u. AJ（u，v）.在这种情况下，实例化AJ（）的连续副本将在不执行任何可见的激活动作的情况下发生在我们向Petri网的转换中，为了产生相同的结果，我们将使用一个特殊的标记等价或无声的调用/取消调用转换（见第5节）。运行示例。使用TOY KLAIM0：：eval（SMR（0））@1. nil 0：：01分 ǁ 1：：12点 ǁ 2：：10分递归过程定义如下：SMR（u1）=dfin（！u）@self。 out（u1）@self. e va l（SMR（sel f））@u. 零。R. Devillers等人理论计算机科学电子笔记154（2006）7177−−−→一（OUT）如果n0 = self，则lJ= l 否则lJ=n0如果n1=self则lJJ=l elselJJ =n1o（l，lJJ，lJ）Ll：：out（n1）@ n0. P−→Ll：：PlJ：：lJ如果n0 = self，则lJ= l 否则lJ=n0如果ni= self，则lJJ= l，否则lJJ= ni（i = 1，.，mA）我我（EVAL）L：：eval（A（n1. nmA））@ n0. Pc（l，A（l，j）. lJJ）、lJ）1mAJJ JJ−−→Ll：：Pl：：{l1/u1. lmA/umA} PA（INVAR）如果n0=self那么lJ=l elselJ =n0i（l，lJJ，lJ）Ll：：in（！u）@ n0。PlJ：：lJ−→Ll：：{lJJ/u}PlJ：：nil（INLOC）如果n0 =self，则lJ= l 否则lJ=n0如果n1=self则lJJ=l elselJJ =n1i（l，lJJ，lJ）Ll：：in（n1）@ n0. PlJ：：lJ−→Ll：：PlJ：：nil（新）lJ∈/Ln（l，lJ）Ll：：ne wloc（u）. P−→L<${lJ}<$l：：{lJ/u}P<$lJ：：nil表3操作语义规则II.2.1操作语义网络和进程的操作语义详见表2和表3。它基于上面定义的结构等价（参见S结构规则）和标记转换规则，这些规则增加了关于已知位置的显式信息。alities（the setsL，LJ <$L）：L<$NactLJ<$NJ，其中act是一个执行前缀和loc（N）{\displaystyle {\loc（N）}}{\DISPLAYSTYLE {\loc（N）}}{\displaystyle {\displaystyle {\loc（N）}}{\displaystyle{\displaystyle {\loc（N）}}{\displaystyle {\displaystyle {\loc（N}}{\displaystyle {\displaystyle {\loc（N）}}{\displaystyle {\displaystyle{\loc（N}}{\displaystyle {\displaystyle {\}}{\displaystyle {\displaystyle{\}}{\displaystyle {\displaystyle}}{\displaystyle{\displaystyle}}{\displaystyle{\displaystyle {loc（NJ））表示在N（resp.inNJ）。 该法可以是o（l，lJJ，lJ）或i（l，lJJ，lJ）或c（l，A（l1，.，lm），LJ）或n（l，LJ），其中初始78R. Devillers等人理论计算机科学电子笔记154（2006）71symbol标识动作的类型，l标识动作执行的位置，lJ标识动作执行的位置，lJJ是参数（动作的自变量）。例如，动作c（l，A（lJJ），lJ）意味着，从位置l，在位置lJ处启动具有有效参数lJJ的进程A的实例，而i（l，lJJ，lJ）记录在l处执行来自位置lJ的输入lJJ。R. Devillers等人理论计算机科学电子笔记154（2006）7179运行示例。在我们的机器人示例中，我们使用i表示位置i，前两个执行步骤具有完整的形式c（0，SMR（0），1）{0，1，2} {0：：e va l（SMR（0））@1. nil0：：11：：22：：0−−→{0， 1， 2}{ 1：：in（！u）@ self。（1）求一个函数。eval（SMR（self））@ u。nili（1，2，1）0：：nil0：：11：：22：：{0，1，2}{1：：out（1）@ self。eval（SMR（self））@2. nil0：：无0：：无1无2：：无0无−−−−−−−−−−−−−→并且可以使用规则PAR，STRUCT和EVAL（第一个）和PAR，STRUCT和IN VAR（第二个）导出。然后，使用中间状态的符号[data in loc0：data in loc1：datain loc2]并省略状态的过程部分以及已知位置L={ 0， 1， 2}的（不变）集合，我们的机器人的执行序列的开始是：c（0，SMR（0），1）[1：2：0]−→【1：2：0】i（1，2，1）−−−−→o（1，0，1）[1：：0]−−→c（1，SMR（1），2）[1：0：0]−→【1：0：0】i（2，0，2）−−−−→o（2，1，2）【1：0：】−−−→【1：0：1】c（2，SMR（2），0）−→[1：0：1]·· ·请注意，机器人的行为在很大程度上取决于存储在本地的初始数据。它可以是确定性的和非终止的（如上所述），确定性的和终止的（如果我们删除初始三个数据项中的任何一个），非确定性的和非终止的（如果我们在初始规范中添加，比如说，0：：020），或者非确定性的和终止的（如果我们在初始规范中添加1：：020并删除0：：021）。3网的代数我们的Petri网模型的发展，称为k-网，受到盒代数[1，2，10]和[9]中用于翻译π-演算术语的p-网代数的启发。特别是，我们使用彩色标记和读弧（允许任何数量的转换同时检查存储在一个地方的资源的存在[6]）。k-网中的变迁有以下标签：（i）o表示将数据输出到数据空间;（ii）i表示从数据空间检索数据;（iii）n表示创建新的局部;（iv）cA表示创建进程A的实例;（v）τ表示辅助静默变迁（仅用于直接过程调用的第一种翻译我们的翻译背后的一个关键思想是将系统视为由一个主程序和一些过程声明组成。我们表示的控制结构的主程序和程序使用不相交的无标记Petri网，一个主程序80R. Devillers等人理论计算机科学电子笔记154（2006）71和每个程序的声明。此外，委员会认为，R. Devillers等人理论计算机科学电子笔记154（2006）7181每个过程调用在Petri网中具有对应的（可能隐藏的）调用转换程序执行一次，而每个过程可以被调用多次（甚至是并发地），每个这样的调用都是通过调用转换的触发来建模的，并且由一个彩色标记唯一地标识，该标记的颜色对应于导致该调用的执行路径上的调用序列。例如，如果t1和t2是同一过程的两个调用转换，则在Petri网中对应于过程声明的令牌t1 t2表示过程的递归调用，其中t2从t1启动。这个路径足以识别一个调用，这是因为一个给定的转换可以被激活多次，但每次都有不同的路径。考虑到这一点，我们使用trailσ的概念来表示过程调用转换的有限（可能是空的）序列（即，图中用cA和τ表示。负责控制网络流的网络的位置携带作为路径的令牌(The用于主程序的空跟踪标记将被视为通常的“黑色”标记。然后，如果标记为cA的转换t的每个输入位置（对于静默调用也类似）包含相同的踪迹标记σ，则过程调用是可能的。然后移除这些标记，并在表示过程PA的网的每个初始（入口）位置插入新标记σt，定义A（. ），以及表示实际参数的其他令牌。k-网中的位置以反映其预期作用的方式进行标记：• 控制流位置：这些模型控制流位置由它们的状态符号标记（内部位置由i标记，接口位置由e和x标记，分别用于入口和出口）。他们携带的标记只是轨迹σ。• 局部位置（或loc-places）：这些携带结构化标记，表示主程序和过程调用已知和使用的局部每一个这样的记号，称为一个尾随局部性，其形式为σ.l，其中σ是一个尾随，l是L中的一个局部性。直观地说，σ标识了令牌可用的调用，而l提供了它的值。在图中，地点有粗边界，并由地点，地点变量和专有名称标记。例如，如果一个loc-placeu包含一个trailed localityσ.l，那么这意味着对应于trailσ的某个过程调用将其locality变量u的值设置为L. 标记为self或selfi的Loc-places表示进程执行的位置• 元组空间位置：这是一个由TS标记的可区分位置，用于表示存储在各个位置的所有数据。它将存储形式为l：：lJ的标记，每个这样的标记对应于进程代数中的l：：lj组件• 新位置的地方：这又是一个著名的地方，由NL标记，并包含所有新鲜的（即，未使用的）局部，然后可以通过N个标记的转换来拾取这些局部，以便体现新的网络局部。所有的位置库所以及元组空间和新位置库所将统称为存储库所。有向弧和读弧由（一个或多个）类型为ω，ω.z，ωt，ωt.x，x，x：：y，z的注释标记，其中ω，x，y，z是（高级Petri网）变量82R. Devillers等人理论计算机科学电子笔记154（2006）71而t是一个（Petri网）变迁名。本文所用的网是带读弧的可组合高级Petri网。定义3.1（无标记）k-网是一个三元组N=（SfSs，T，i），其中：Sf和Ss分别是控制流和存储库位的不相交的有限集合;T是与Sf和Ss不相交的变迁的有限集合;i是为库位、变迁以及库位和变迁之间的弧定义的注释函数弧可以是有向的（在（（Sf<$Ss）×T）<$（T×（Sf <$Ss））中）或无向的（在{{s，t}中）|s ∈（Sf<$Ss）<$t ∈T}）。假设以下成立：• 对于Sf中的每个控制流位置s，i（s）是一对（λ，D），其中λ∈ {e，i，x}是给出位置状态的标签（分别为入口、内部或出口），确定其在复合算子应用期间的作用第二个组件D是s的类型集，这意味着s只能包含来自集合7D的标记。在下文中，我们分别用N和N表示N的入口位置和出口位置的集合（形成k-网的入口和出口接口）。• 对于Ss中的每个商店位置s，i（s）是一对（λ，D），其中λ是标签（例如TS或NL或位置），并且D再次是s的类型集，这意味着s只能包含来自集合8D的标记。N中至多允许存在一个具有给定标签λ的存储库位。• 对于T中的每一个t，ι（t）是一个标签--一个带有变量的项--表示当跃迁触发时从外部可见的东西（具体的标签将在后面介绍）。 转换标签的一个示例是具有变量z、y和x的项i（z，y，x）。直观地说，transition label可以被认为是从变量绑定到KLAIM前缀的函数。• 对于每个弧a，无论是无向的（a={s，t}）还是从一个地方到一个过渡的（a=（s，t））或从一个过渡到一个地方的（a=（t，s）），i（a）都是一个注释，它是一组带有变量的项（具体的注释将在后面介绍）。弧注释中使用的术语的示例是变量ω或元组（对）ωt.x，其中ω和x是变量。像往常一样，我们将只绘制带有非空注释的弧（注释函数i返回空集的弧被视为不存在）。我们还将假设每个变量都有一个可能值的相关域，并且对于每个转换t，如果{t1，. ，n}表示出现在t的标签中和与t相邻的弧上的变量，我们将用b表示绑定，该绑定在其域中为每个变量ni分配值。我们将只考虑以下法律约束，即，使得对于t和s之间的每个弧a，如果k∈i（a），[6]在我们的翻译中，无向弧只将存储库位连接到转换，但这里给出的定义允许更多的可扩展性。7在我们的翻译中，D ={σ|σ is a trail}，意味着s只能包含trail，即，控制流令牌。8在我们的翻译中，对于局部位置，D ={σ.l| [001 pdf 1st-31 files]σ是踪迹，l是地点};对于TS地点，D={l：：lJ} |l，lJ是地点};对于NL地点，D是所有地点的集合。R. Devillers等人理论计算机科学电子笔记154（2006）7183t，int，outt，int，in在约束b下的k（表示为b（k））将提供s中允许的值。此外，在约束b下激发的跃迁的观察到的标记将由b（i（t））表示。动力学一个转换可以在绑定映射下被触发，b为它周围发生的变量赋值。然后，转换必须“检查"a b s或b”或“p r”的存在，这取决于b（ω），b（ω）.b（z），b（ω）t，b（ω）t .b（x），b（x）：：b（y）n的k。一个k-网N的标记M是一个函数，它给每个位置s分配一个属于它的类型的标记的多重集一个有标记的k-网将被表示为（N，M）。下面我们用g和g分别表示多集和差。此外，如果M和MJ是同一元素集Z上的多重集，则M ≥MJ将意味着M（z）≥MJ（z），对所有z∈Z。设M是N的一个标记，t是任意的转移，b是t的一个约束。然后我们用Mbbt，出局 两个标记使得对于每个位置s，bt，in（s）={b（k）}和Mbk∈i（（s，t））（s）={b（k）}。k∈i（（t，s））将启用转换t（即，如果在约束力B下允许发射，对每个位置s∈Sf <$Ss，M（s）≥Mb（s），而且对每个k∈i（{s，t}）.然后可以触发一个使能的t，它将M转换为一个新的标记MJ，使得对于每个位置s∈Sf <$Ss：MJ（s）=M（s）g Mbbt，出局 （s）。b（i（t））这将由（N，M）−→（N，MJ）来表示，并且这一类型的移动将在由初始标记生成的k-net标记转移系统的定义例如，在图5中，跃迁t1可以在绑定k ={ω <$→ 0，x<$→1，x1<$→0，z<$→ 0}下触发。它的发射消耗入口处的令牌，检查令牌的存在。0，0，0。1、。0分别在loc-placeself1、1和0中，并产生：在最左边的内部位置中的t1-token，在上部内部位置中的t1-token，t1。1-在place self SMR中的令牌，并且t1。0-令牌在位置u1。因此，我们有：（N，M）c（0，SMR（0），1）−→（N，MJ）其中两个标记的k-net如图5所示。复合算子由于翻译是语法驱动的，我们需要与TOY KLAIM中的操作符相对应的操作符，允许组合地构建k-网。这些运算符是prefixing（N。 N J）、选择（N + N J）和平行合成（N |N J）。特别地，所有三个运算符合并存储位置（即，loc-places、TS和NL），同时将它们周围的弧和弧注释保持在N[10][11][12][13][14][15][16][17][18][19]对于两个操作数网，在应用和MDFMDF（s）喀麦隆84R. Devillers等人理论计算机科学电子笔记154（2006）7122复合操作符，以便允许适当地处理当，例如，N=NJ。在选择合成中，类似于盒代数[1]中的选择运算，N和NJ的入口和出口位置通过一个卡累利阿积组合在一起。这具有以下效果：如果我们从每个入口位置包含公共踪迹标记σ的副本的情况开始，则可以在该踪迹下执行N或NJ前缀运算符将前缀N的出口位置与Nj的入口位置组合成内部位置，结果是N在到达终端标记（其中唯一的出口位置被标记）之后执行，然后执行N J。N和NJ的并行组合将它们并排放置，允许并行执行两个部分我们将用于组合k-网的算子是PBC及其各种扩展中定义的适当调整的实例[1，10]。特别是，在组成网络时处理存储位置的方式直接受到APBC [10]的异步通信结构的启发。在下文中，我们假设Ni=（SfSs，Ti，ii）（i= 1， 2）是两个不相交的我我无标记k-网，使得对任意s1∈Ss和s2∈Ss，如果ι1（s1）=（λ，D1）且1 2i2（s2）=（λ，D2），则D1=D2，即，以同样方式标记的商店也有相同的类型设置。接下来要定义的操作都如图2所示。prefixing. N1. N2定义为如果N1有唯一的e-位置和唯一的x-位置，并通过以下程序获得：•N1和N2并排放置。• 对于每个s2∈N2，我们创建一个新的位置SJ，其状态为i，并且每个对于i∈ {1， 2}，si和t∈Ti之间的弧a被替换为sJ之间的同类弧（指向或来自，或无向）和具有相同注释和t.然后删除N1中仅有的x-位s1和N2中仅有的e-位• 具有相同标签和相同类型的商店位置被“合并”到具有相同标签和类型的商店位置中，并且将它们链接到N 1和N 2中的转换的选择 N1+ N2通过以下步骤获得：•N1和N2并排放置。• 对于每一个s1∈<$N1和每一个s2∈<$N2，我们创建一个新的位置s，其状态为e，并且使得在si和t∈Ti之间的每一条弧a，对于i∈ {1， 2}，被替换为在s和t之间具有相同类型（指向或来自，或无向）和相同注释的弧。类似地，对于每一个s1∈N和每一个s2∈N，我们创建一个新的位置s，1 2状态x和连接性定义如上。然后删除N1和N2的e-位和x-位• 具有相同标签的商店位置与prefix的情况一样被平行组合。 N1|N2通过以下程序获得：R. Devillers等人理论计算机科学电子笔记154（2006）7185N1ω.yω.zωωN2ω.yω。不ωωαω.zω.yω.yω。不我ωωωωωβω.zαω.yω.yωγωω。不ωαβαγe x e xβγN1. N2exN1+N2exXN1|N2X图2.在k-net上定义的各种运算符的说明（省略了转换标签，因为它们不受三个运算的影响）。•N1和N2并排放置。• 具有相同标签的商店位置与prefix的情况一样被4将网络转换为Petri网我们假设下面的索引良构网络N要被翻译：. 吕Σli：：Pi.克什蒂尔克ΣlJ：：ljji=1j =1j j连同必要的过程标识符定义;我们还假设li/=liJ，为i iJ。注意，h或k可以是0，在这种情况下，中间不存在。我们还假设，每个进程标识符A在网络或进程定义中至少出现一次。基本动作图3给出了玩具KLAIM的基本动作的翻译。输入操作。我们有两种不同的翻译，这取决于所使用的模板的形式。第一个，K（in（nJ）@n），必须在元组空间位置TS中为所考虑的轨迹找到对应于n和nJ的当前值的匹配对，以及eωωω.z ω.yβαγω.yω.不eωω86R. Devillers等人理论计算机科学电子笔记154（2006）71eω.xωt.xωω.zCAω.x1不ωtωt.x1.ω.xmAXωωt.x是个.neω.xω x：：yOTSω.yωω.znJx自我eNLuωxω.xnωω.zX自我neTSω.xω x：：y我ω.yωω.znJx自我neTSω.xω x：：y我ω.yωω.zux自我K（in（nJ）@n）K（in（！u）@n）K（out（nJ）@n）K（newloc（u））nselfA自我n1eAeu1自我nmAumAK（eval（A（n， . n））@n），其中A（u， .. . ， u）=dfPXK（零）1mA1mAA图3.基本动作的翻译。在这里和后面，跃迁标签以缩写形式给出：ist和sfori（z，y，x）;oforo（z，y，x）;nforn（z，x）;以及dcAinthisc as forc（b（z），A（b（x1）， . . . ，b（xmA）），b（x））.只有这样，该动作才能被执行（结果是匹配的对x：：y_x从元组空间位置消失）。 我们不假设nJ，n和self是不同的，如果它们中的一些是相同的，我们折叠相应的loc-places，并收集在一起（通过联合）相应的读弧的注释。在极端的情况下，对于K（in（self）@ self），三个loc-place 被折叠成一个单独的loc-place，标记为self，连接它和唯一的跃迁的读弧被注释为ω.x，ω.y和ω.z。请注意，x表示输入的位置（nJ），y表示输入数据（nJ），z表示执行输入的位置（self）（当执行时，这将在转换的可见标签中使用）。第二个翻译，K（在（！u）@n），其中u是变量，类似地工作，除了在元组空间位置TS中对应于针对所考虑的踪迹在n中观察到的局部性的值（之一）被存放在局部位置u中。我们不假设n和self是不同的（而u是一个绑定变量，是不同的），如果它们是相同的，我们折叠相应的loc-places，并将读取弧的注释聚集在一起。R. Devillers等人理论计算机科学电子笔记154（2006）7187DF当在绑定b下触发时，在这两种情况下，平移都生成可见标签i（b（z），b（y），b（x））。产出行动。在K（out（nJ）@n）中，我们不假设nJ，n和self是不同的，如果它们中的一些是相同的，我们折叠相应的loc-places，并将相应的读弧的注释聚集在一起n和nJ的含义与输入动作的第一种形式相同，但这里在元组空间位置产生一对x：：n j当在绑定b下触发时，网络生成可见标签o（b（z），b（y），b（x））。新地点。在K（newloc（u））中，在绑定b下执行转换生成可见标签n（b（z），b（x）），并且从新局部位置获取新位置b（x）并将其插入位置u。过程创建。 翻译K（eval（A（n1，. ，nmA））@ n）假设A的定义方程是A（u1，. ，μmA）= PA. 我们不假设self，n和n1，. ，nmA是不同的，并且如果它们中的一些是相同的，则我们折叠相应的loc-place，并且将相应的读取弧的注释聚集在一起。 另一方面，自我A，u1，. ，umA和eA都是不同的。 在极端情况下，对于K（eval（A（self，. ，self））@ self），左边的m个A+2个loc-places被折叠成一个单独的loc-places，标记为self，连接它和唯一的transition的读弧被注释为ω.z，ω.x，ω.x1，. ，ω.xmA.进程创建的思想是在子网中生成一个新的活动线程，该活动线程与进程标识符定义相对应。特别地，参数U1，.，umA 的当前位置值对应的值n1，.，nmA （注意，线程的新特性是通过扩展在t的左边有标记的痕迹，使它们与其他标记不同）。此外，标记为eA的辅助位置稍后（参见下面翻译的第三阶段）将用于启动与该激活实例的过程标识符定义相对应当 在绑 定 b 下激 发时，平 移生 成可见 标签 c（ b（z ）， A（b （x1），. . ，b（xmA）），b（x））.零过程。平移K（nil），没有任何过渡，有三个地方共同的所有基本翻译。4.1翻译一阶段对于每个i≤h，因此对于每个li：：Pi分量，我们首先在成分上平移Pi（即，同态地）转化为K（Pi）。请注意，虽然e表示控制位置，但eA不表示，因此在各种网络结构中会合并之后，我们将（唯一的）位置标签self更改为selfi。结果表示为K（li：：Pi）。另请参见图4左侧的运行示例阶段I的结果DF第二阶段。对于每个过程定义A（u1，.，μmA） =PA，我们首先翻译将PA转化为K（PA）。之后，我们为每个元素添加标记为ui的i≤mA，除非这样的位置已经存在。 最后，我们重新给唯一的自我贴上88R. Devillers等人理论计算机科学电子笔记154（2006）71loc-place到selfA，如果有另一个loc-placeselfA存在9，我们将它们合并。结果记为K（A）。另请参见图4右侧的运行示例的阶段II的结果。第三阶段。我们采用K（A）然后，如果K（A）有r个入口位置，我们创建（唯一的）eA标记位置的r个副本，并将它们与K（A）的入口位置标识（具有与eA标记位置相同的输入弧和与K（A）的入口位置相同的输出弧）。然后，我们将K（A）的入口和出口位置转换为内部位置。之后，我们将初始标记设置如下：对于i≤h，我们将i.li插入到自i-标记的位置（i表示空的踪迹）;由局部l∈L标记的每个位置（我们假设对于每个i，selfi/∈L <$U）对于每个可能的踪迹σ接收标记σ.l;每个入口位置接收单个标记σ.l;对于每个l∈ L\L，我们将单个标记l插入将单个令牌lJ：：rlJJ插入到TS标记的位置中，如果尚未创建J J存在（除非k= 0）。整个平移的结果将由PN（N）表示。注意，到目前为止，还没有使用τ跃迁可以观察到，恒定定域位置的初始标记是无限的，因为有无限多个可能的σ 这是因为，我们需要允许进程的每个可能实例都可以使用这样一个显式的局部性（相反，对于局部性变量位置，标记最初是空的，当特定绑定下的转换被触发时，标记会逐渐插入）。然而，还有一种更简单的翻译，它依赖于区分变量的局部位置和显式局部性或图3的基本翻译中的自局部性：人们只需将这样一个显式局部性位置l周围的读弧上的ω.x类型的注释（在图3中，可以看到没有定向弧到达或来自这样一个位置）替换为x，并将