局部动作系统建模Petri网编码的分析研究

电子笔记在理论计算机科学50第3期（2001年）。GT-VMT 2001网址：http://www.elsevier.nl/locate/entcs/volume50.html7页用局部动作系统建模Petri网1尼科·韦林登2安特卫普大学数学与计算机科学系比利时安特卫普Dirk Janssens3数学与计算机科学系Universitaire Instelling Antwerpen比利时安特卫普1引言在描述并发系统的形式化模型中，Petri网无疑是最流行的一种。他们有一个有吸引力的视觉presentation，和丰富的理论已经发展为他们[8，9]。多年来已经提出了几种类型的图重写系统，包括代数图文法[3]和局部作用系统[5]。后者的理论是基于一个过程的概念，一个描述系统运行的节点是congurations的节点和因果关系是由这些节点上的偏序表示本文的目的是探讨局部行动系统改写离散图对Petri网的编码，特别是对Petri网的标记选择不同的编码方式的影响。 结果表明，系统具有与网相同的顺序行为，但具有不同的并发行为。事实证明，两个特定的选择（令牌和位置表示）对应于众所周知的Petri网类。随后，考虑了一个应用程序，其中网络的并发行为1 由 EC TMR 网 络 GETGRATS （ 图 形 转 换 系 统 的 一 般 理 论 ） 和 Esprit 工 作 组APPLIGRAPH通过Universitaire Instelling Antwerpen提供部分支持。2 电子邮件：Nico. ua.ac.be3 电子邮件：Dirk. ua.ac.bec2001年由Elsevier Science B出版。V.CC BY-NC-ND许可下的开放访问。2xygGT-VMT 2001 { N. Verlinden和D. Janssens随着时间的推移而变化，它表明，这种情况可以使用所提出的编码处理。因此，虽然这并不奇怪，Petri网可以建模的局部行动系统，有证据表明，后者过于充足的灵活性，作为一个统一的框架，一些众多的变种Petri网。此外，局部动作系统本身就是一种描述并发系统的强大语言。2地方行动系统（LAS）首先回顾了LAS图重写的一些基本思想。局部动作系统是一种基于节点重写和嵌入的图重写系统，在[5]中引入。本文只考虑离散图被重写的非常有限的情况在LAS中，假设节点标签的集合形成交换幺半群。一个产品包括一个带标号的离散图L，一个标记的离散图R，对于每个对（x; y），其中x是l的节点，y是r的节点，节点标签上的动作ax;y。在LAS中，动作的局部性意味着动作的输入和输出都对应于一个节点。一个动作只局部地影响一个图为了应用于图g，我们有：（1）找到g的一个子图l0，它与l匹配;（2）用新节点替换l0的节点，r的每个节点对应一个新节点;（3）计算新节点的标号。如果新节点y 0对应于r的节点y，则其标号是y在r中的标号与所有标号a的和（lab（x0）），其中x是l的node，x0是对应于x的g的node，并且labg（x0）是其la bel。假设节点标签的集合具有偏序.图l匹配图l 0，如果存在从l的节点集到l 0的节点集的双射函数f，使得对于l的每个节点x，f（labl（x））labl0（x）。因此，matchingdep的概念以选择.一个局部动作系统由一个图和一组产生式组成3Petri网带弧权重的标记位置/转换网络，简称标记网络，是第一种类型的Petri网考虑，这是众所周知的，各种变种的Petri网可以建模的标记网。图1描绘了标记网。在这篇摘要中，我们将注意力限制在所有权重都为1的情况下标记网的一个状态是一个标记，而在图重写系统中，3GT-VMT 2001 { N. Verlinden和D. Janssenss2发送1c1接收1r2生产队列s3s1第二阶段R3c2接收2出队消费r1Fig. 1.标记位置/转换网络。状态是一个图。如果想通过图重写系统对标记网进行建模，则每个标记都需要一个图表示。考虑以下三种类型的图形表示图的每个节点表示标记的一个令牌。图中的每个节点代表一个地点。图中的每个节点代表一组地点。图2示出了标记的三个不同的图形表示，其表示为1个标记在位置s2，2个标记在位置s3，以及1个标记在位置r2。从形式上讲，（一）（b）第（1）款（c）第（1）款s1;0s2;1c1;0r1;0r2;1s 2; 1第3条;1第3条;1第2条;1s1;0s2; 1s3; 2c1;0c2;0r3; 0r1; 0r2; 1s3;2c2;0r3; 0图二. 标记的不同图形表示nodela表示v=[S*Z]的元素，即， 从位置集S到Z的部分函数的幺半群，其中f+ g的域对于2个部分函数f和g是f和g的域的并. 图2（c）位置集合被分成组fs1; s2; s3g，fc1; c2g和fr1; r2; r3g。例如，在一个示例中，图中最左边的节点的标签2（c）表示具有域的部分函数，其位置为fs1; s2; s3g，并且将s1映射到0，s2映射到1，并且s3映射到2。本文证明了不同的图表示产生局部动作系统，使得它们的顺序行为相同，但它们的并发行为不同。通过这种方式，人们可以通过局部动作系统获得同一标记网络的本文所考虑的所有系统，Petri网以及局部动作系统，都有一个过程语义，每个过程确定一组序列化。由于在所有情况下，系统要么是Petri网，要么是Petri网的LAS编码，这些序列化可以被视为[2]意义上的发生序列。因此，人们可以使用下面的等价概念来比较系统，特别是它们的并发行为。定义3.1设P和P0为过程。P和P0是等价的，如果它们确定相同的出现序列集合.4设N和N0为系统。N和N0是过程等价的，如果对于N的每个过程P，存在N0的等价过程P0，反之，对于N0的每个过程P0，存在N的等价过程P。5GT-VMT 2001 { N. Verlinden和D. Janssens现在更详细地考虑这些标记的不同表示导致不同局部作用系统3.1标记表示在第一表示中，图的每个节点精确地表示标记的一个标记。这种表示可能是最直接的，并且已经在[1]中进行了研究。转换由产生来建模，使得左手侧是由转换消耗的令牌的图形表示，并且右手侧是由转换产生的令牌的图形表示。图3描绘了图1中的标记网的三个转变的1.一、的虚线（一）s2; 1（b）第（1）款s1; 1（c）第（1）款第2条;第3条;第1条s1; 1第2条;第3条;第1条r1; 1图三.生产建模的转变（a）生产，（b）排队，（c）出队。描述因果关系。所有的局部动作都是0，即v上的函数将每个节点标签映射到v中的部分函数中，并且具有空域，因此它们没有被描绘。事实证明，以这种方式获得的局部动作系统与它编码的标记网络具有相同的顺序和并发行为。(see[4]）。定理3.2设N是一个标记网，N0是它的（令牌）编码.那么N和N0是过程等价的。3.2地点表达在第二种表示中，标记网的每个位置对应于图的一个节点。每个转换都改变了几个地方的令牌数量，因此对转换t进行生产建模必须重写与t的输入或输出位置相对应的每个节点。在rst方法中，等式用于确定匹配的偏序。由于每个地方的令牌数量可能会有所不同，因此转换是由一组产生式进行建模的。图4描绘了对图1中的标记网的转移队列进行建模的几个产品。例如，图4（c）中的生产（一）s 1;1s2;0s3;0（b）第（1）款s 1;2s2;0s3;0（c）第（1）款s 1;1s2;0s3;3（d）其他事项s 1;2第2条;第1条第3条;第5条s1;0s2; 1s3; 1s1; 1s2; 1s3; 1s1; 0s2; 1s3; 4s1; 1s2; 2s3; 66见图4。 对转换队列进行建模的产品的数量。7GT-VMT 2001 { N. Verlinden和D. Janssens可应用于对S1中的1个令牌、S2中的无令牌以及S3中的3个令牌进行建模的图。结果，s1的令牌被拿走，并且1个令牌被添加到s2和s3，从而在s2中产生1个令牌，在s3中产生4个令牌。显然，这样得到的局部动作系统有一个不完备的产生式集。通过引入非零局部动作并使用另一个偏序来定义匹配，可以得到它的一个nite版本。 如果对应的局部动作不为0，则因果关系的虚线被实线代替。在图中，有3条实线标记为本地动作1，表示身份。因此，这种生产可以应用于任何图形，其中至少有一个令牌模型在s1（一个选择的有效性的关系上的一组部分功能，从地方到Z）。由于将本地操作与右侧相结合，s1的一个令牌被拿走，并且一个令牌被添加到s2和s3。有以下定理。定理3.3设N是有标记网。设N0是它的nite位置编码，并且设N 00是它的nite位置编码。 那么N 0和N 00是过程等价的。通过这种编码，只有当它们不重写相同的节点时，即只有当它们所建模的转换的位置不重叠时，才可以并发地应用两个产生式。因此，标记网络的位置可以被看作是一次只能由一个转换访问的资源。这种情况也会发生在基本网络中，因此可以用这种方式对无接触基本网络进行建模。定理3.4设N是一个无接触的初等网系统，N0是它的（nite或inite）位置编码.那么N和N0是过程等价的。3.3地点组别的代表性为了进一步说明LAS机制的灵活性，考虑图1的标记网的并发行为被进一步限制的情况：假设地点被分组在一起，并且每组地点一次只能被一个转换访问。这种情况出现时，一个有一定数量的内存块由处理器管理，一个分配每个内存对象（地点）的内存块（处理器）。通过这种方式，转换不会锁定一个位置，而是整个街区。在s1、s2属于同一组但s3不属于同一组的情况下，转换队列可以通过图1的产生来编码5（b）.人们可以更进一步，对一个地方从一个群体到另一个群体的可能迁移建模。然后，可以对每个地点p使用一个迁移程序（见图2）。 5（c））。图中局部作用p~和p分别表示部分函数对fpg和p的补的限制。通过应用这样的产生式，人们改变了地点的分组（从而改变了并发行为）。8p~pGT-VMT 2001 { N. Verlinden和D. Janssens（一）（b）第（1）款（c）第（1）款s1;1 s2;0s3;0s1; 1s2;0 s3;0;;1111 11第1条;第1条第2条;第1条s3; 1s1;1s3;1;s2;1图五.（a）和（b）中的不同地点分组，以及（c）中的地点迁移。结论和今后的工作结果表明，局部行为系统是一个灵活的建模框架不同类型的Petri网和不同视图的Petri网建模的并发性。除了考虑Petri网的其他和可能更复杂的变体（例如，抑制剂网）它可能是有趣的发展一种更高层次的过程理论，从系统的具体细节中抽象出来，如Petri网或局部行动系统。通过这种方式，人们可以得到一个框架，其中可以研究包括Petri网和各种类型的图重写系统在内的一大类系统的顺序和并发行为。引用[1] A. Corradini，并发计算：从Petri网到图形文法，在联合图形重写和计算研讨会（SEGRAGRA'95）的会议记录中，理论计算机科学电子笔记，卷。 2，Elsevier，1995.[2] J. Desel和W.Reisig，Place/Transition Petri Nets，In [9]，122-173.[3] H. Ehrig，M. Kor和M. Lowe，《Introduction to the Algebraic Approach ofGraph Grammars based on Double and Single Pushouts》，2004年。第四届国际图形语法及其在计算机科学中的应用研讨会论文集，计算机科学讲义，第532卷，Springer-Verlag，柏林，1991，24-37。[4] 联 合 Goltz 和 W. Reisig ， Processes of Place/Transition - Nets ， InAutomata ， Languages and Programming ， Lecture Notes in ComputerScience，Vol. 154，Springer-Verlag，Berlin，1983，264-277.[5] D. Janssens ， Actor Grammars and Local Actions ， 在 Handbook ofGraph Grammarsand Computing by Graph Transformation ， Vol.3 ，World Scienti c，1999，57-106.[6] K. Jensen，着色Petri网的理论介绍，在并发的十年中，计算机科学讲义，第803卷，Springer-Verlag，柏林，1994年，230-272。9GT-VMT 2001 { N. Verlinden和D. Janssens[7] Kleijn和M. Koutny，Process Semantics of P/T-Nets with Inhibitor Arcs.在Petri网的应用和理论，计算机科学讲义，第1825卷，Springer-Verlag，柏林，2000年，261-281。[8] W.李文，《计算机科学与工程》，北京，1998。[9] W. Reisig和G. Rozenberg，（eds.）. Petri Nets I：Basic Models（Petri网基本模型）在Petri网的进展，计算机科学讲义，第1491卷，Springer-Verlag，柏林，1998年。[10] G. Rozenberg和J. Engelfriet，Elementary Net Systems，[9]，12-121。