有限跃迁系统的正交模偏序集及其在Petri网中的建模

理论计算机科学电子笔记270（1）（2011）147-154www.elsevier.com/locate/entcs关于由转移系统生成的正交模偏序集LucaBernardinello1LuciaPomello1StefaniaRombol`a1Universit`adeglistudidi摘要我们研究由有限跃迁系统的几组状态形成的正交模结构。这些集合称为区域，可以解释为分布式并发系统的本地状态，可以对其进行建模一个Petri网主要结果表明，这种正交模结构有足够的元素来表示某些元素子集的交。关键词：并发，Petri网，正交模偏序集，量子逻辑1引言研究了一类由有限自动机产生的正交模结构。这种结构的元素被定义为自动机状态集合的某些子集。这些子集可以被解释为局部状态，与自动机的给定全局状态相反，在某种意义上，这将在下面解释。这一系列的研究来自于我们对Petri网理论的兴趣，这是一种并发和分布式系统的形式模型，由Carl Adam Petri引入，旨在建立一种体现现代物理学原理的系统理论，特别是狭义相对论和量子力学（[4]）。Petri网根据局部状态（条件）和状态的局部变化或事件（[5]，[6]）对系统进行建模。事件的完全特征在于它们的发生在系统的局部状态中所产生的变化：在事件e发生之前为真而在事件e发生之后变为假的条件是事件e的先决条件，而为假而变为真的条件是后置条件。1这项工作得到了MIUR的1571-0661 © 2011 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2011.01.013148L. Bernardinello et al. /Electronic Notes in Theoretical Computer Science 270（1）（2011）147通过这种方式，该模型明确地捕获因果依赖关系，用因果顺序代替时间顺序，并用并发代替并行性。基于这些简单的元素，Petri定义了一个本质上异步的计算模型，并赋予了一组通用的可逆逻辑门。基于特定的操作语义，Petri网理论后来也在其他方向上得到了发展：局部状态的某些集合形成了系统的潜在全局状态;系统的行为可以由建立在全局状态上的有限状态自动机（或转移系统）来描述，其中状态转移由局部事件的名称来标记在本文中，我们提出了一些结果对类的正交模结构产生的有限自动机，描述的条件和事件的网络，形成了一个基本类的Petri网的行为的特征。2初步定义在本节中，我们将介绍以下所需的基本定义。2.1条件事件网络系统条件事件网系统（简称CE网系统）是由Carl Adam Petri（[5]）作为一般系统的基本模型定义2.1一个网是一个三元组N=（B，E，F），其中B和E是有限集合，F（B×E）（E×B），以及(i) BE=;(ii) dom（F）ran（F）=BE.B的元素称为局部状态或条件，E的元素称为状态或事件的局部变化，F称为切流关系。对于每个x∈B<$E，定义·x={y∈B<$E|（y，x）∈F}，x·={y∈B<$E|（x，y）∈F}.对于e∈E，如果b∈·e，则元素b∈B是e的先决条件;如果b∈e·，则它是e的后置条件。一个网N=（B，E，F）是单的，对于每个x，y∈B<$E（·x=·y和x·=y·）<$x= y; N =（B，E，F）对每个e ∈ E·e <$e·=<$是纯i <$。给定一个网N=（B，E，F），定义K=IP（B），其中IP（X）表示X的幂集。 K的元素称为N的格。 一个事例是N所模拟的系统的转换的发生，这是受触发规则，定义如下，改变当前的情况。设m1，m2<$B是N的两种情形，e∈E是事件.我们可以说，e在m1处的出现将网系统从m1带到m2，记为m1[e<$m2，如果·e m1，e·m1=，m2=（m1\·e）e·.当m1[e]<$m2时，对某个e∈E，我们说m2是从m1向前一步可达的。 我们称ρ为一步向前可达关系。 则（ρ <$ρ−1）<$是N的完全可达关系。L. Bernardinello et al. /Electronic Notes in Theoretical Computer Science 270（1）（2011）147149定义2.2条件事件网系统（CE网系统）是一个四元组N=（B，E，F，C），其中（B，E，F）是一个简单的纯网，C是完全可达关系的等价类。C的元素称为可达情况CE网系统的语义可以用几种方式定义。用顺序事例图给出了一种操作语义。定义2.3CE网系统N的序贯事例图是三元组SCG（N）=（C，E，T），其中T ={（c1，e，c2）|c1，c2∈ C，e ∈ E，c1[e<$c2}.不同的网络系统在这个语义上是等价的，因为它们生成同构的情况图。对于任何CE网络系统，都存在一个等效的CE网络系统，该系统是饱和的地方状态（条件），如Eschericht和Rozenberg（[3]）所示。定义2.4设N=（B，E，F，C）。则存在N=（B，E，F，C）使得：(i) SCG（N）同构于SCG（N≠）(ii) BB和 FF;(iii) N是饱和的，也就是说，不可能在不生成非简单网或不改变N的行为的情况下向B添加新的条件。饱和网系统的局部状态集可以被赋予一种偏序，对应于一种逻辑蕴涵形式。定义2.5设N=（B，E，F，C）是一个CE网系统。b1，b2∈B：b1≤Nb2惠益c∈C：b1∈c<$b2∈c.本文讨论了在N≠ 0的条件下，由≤N2.2变迁系统我们首先定义感兴趣的有限状态自动机定义2.6变迁系统是一个结构A=（S，E，T），其中S是一组状态，E是一组事件，T是一组变迁。一个过渡系统是有限的，如果S和E是有限的。 在论文的其余部分， 将只考虑满足以下公理的有限变迁系统(i) 转移系统的底层图是单连通的;（ii）n（s1，e，s2）∈T：s1/=s2;(iii)<$（s1，e1，s2），（s1，e2，s3）∈T：s2=s3<$e1=e2;（iv）E∈E： n（s1，e，s2）∈T.区域是一组状态，使得给定事件的所有出现相对于该区域具有相同的交叉关系（进入、离开或不交叉150L. Bernardinello et al. /Electronic Notes in Theoretical Computer Science 270（1）（2011）147∈这一点，对于所有的事件都是适用的[3]。 区域可以被解释为系统的局部状态，其行为由过渡系统描述。这样的局部状态对应于在全局状态中为真或假的条件。区域r是对应条件为真的全局状态的集合定义2.7设A=（S，E，T）是一个过渡系统。一个状态集rS被称为是一 个 环ionie∈E，（s1，e，s2），（s3，e，s4）∈Tw e have（s1∈rs2∈/r）（s3∈rs4∈/r）（s1∈/rs2∈r）（s3∈/rs4∈r）。A的所有区域的集合将由RA表示。从定义中可以得出：S∈RA和S\r∈RA：S\r∈RA。对于每个s∈S，Rs表示包含s的区域的集合。定义区域的条件允许我们将事件和区域之间的交叉关系形式化。这是通过区域的前集合和后集合以及事件的前集合和后集合的概念来捕获的。定义2.8设A =（S，E，T）是一个过渡系统。 设rR A. 则r的前集，用·r表示，r的后集，用r·表示，定义为：·r ={e∈E| <$（s1，e，s2）∈T：s1r and s2∈r}，r·={e∈E| n（s1，e，s2）∈T：s1∈r 和 s2/∈r} 。 设 e∈E. 然 后 ， 分 别 用 ·e 和 e· 表 示 的 e 的 前 集 和 后 集 定 义为：·e={r|r∈R A且e∈r·}，e·={r|r∈R A和e∈·r}.现在我们准备给出条件事件转移系统（CE转移系统）的定义，它形成了与CE网系统的序列事例图定义2.9有限变迁系统A=（S，E，T）是条件事件变迁系统（CE变迁系统），它满足以下公理：A1. s1，s2∈S：Rs1=Rs2，s1= s2;A2. s∈Ss∈S<$e∈E：e·R s<$s1∈S（s1，e，s）∈T.CE网系统的序贯事例图是CE变迁系统。反之亦然，给定一个抽象的CE变迁系统A=（S，E，T），总有可能构造一个CE网系统N（A），使得它的序列情况图同构于A。N（A）的条件是A的区域，N（A）是条件饱和的.2.3正交模偏序集正交模偏序集可以看作是布尔代数的一种推广，其中的交和并是部分运算，而每个元素都有一个补。定义2.10一个正交模偏序集P = P，≤，0，1，（.）是一个偏序集<$P，≤ <$，有一个最小和一个最大元素，分别用0和1表示，有一个映射（. ）P：P→P，使得以下条件被验证（其中，P和P分别表示最小上界和最大上界L. Bernardinello et al. /Electronic Notes in Theoretical Computer Science 270（1）（2011）147151关于≤的下界，当它们存在时）：<$x，y∈P（x）n=x;x≤yy≤x;x≤y<$y=x<$（y<$x<$）;x≤y<$$>x <$y∈P;xx= 0。上述第三个条件称为正交模定律。正交模偏序集P的两个元素x，y是正交的（记为x<$y）当且仅当x≤y <$$>;x和y是相容的（记为x$y）当有三个元素x0，y0，z∈P是成对正交的，使得x=x0<$z和y=y0<$z。 一个正交模偏序集P是相干的，如果对所有的x，y，z∈P，两两相容，它保持（x<$y）$z。在下文中，我们将使用OMP作为正交模偏序集的简写。我们感兴趣的是OMP的某些子集，这里称为素滤波器，它可以被看作是布尔代数中超滤波器的推广。 它们对应到量子逻辑文献中定义的二值状态（例如，见[7]）;为了我们的目的，将它们视为子集而不是映射是方便的定义2.11设P = P，≤，0，1，（. ）你是一个OMP。一个非空子集f∈P对所有x，y∈P，是素滤波器i ∈：(i) （x∈f且x≤y）(ii) （x，y∈fandx $y）<$x<$y∈f(iii) 0/∈f(iv) <$x，y∈P：（x$yandx <$y∈f） <$（x∈fory ∈f）P的所有素滤波器的集合将被表示为FP（P）。对于x∈P，[x]将表示P的所有包含x的素滤子的集合。我们称一个OMP为P素数，如果素过滤器的集合有足够的元素来3区域正交模偏序集设A=（S，E，T）是一个转移系统. A的区域集合是由集合包含偏序的。由此产生的偏序集有一个最小值，空集，和一个最大值，所有状态的集合S。我们实际上可以证明它是一个凝聚的素正交模偏序集（见[1]）。我们将这个偏序集表示为H（A）=（R A，n，（.），S）。一般来说，H（A）不是格。若A是CE变迁系统，则H（A）是布尔代数，仅当A能被实现为状态机网系统的事例图，即CE网系统，使得任何事件只有一个前置条件和一个后置条件，且每个可达事例只包含一个条件.152L. Bernardinello et al. /Electronic Notes in Theoretical Computer Science 270（1）（2011）147当A是CE转移系统时，它的状态与H（A）的素滤子之间存在强关系。设s∈S;包含s的区域集合是RA的素滤子;这个素滤子将用fs表示。另一方面，一般来说，H （ A ） 的 所 有 素 滤 波 器 都 对 应 于 A 的 态 。尽管如此，我们可以把所有过滤器解释为另一个跃迁系统的状态，A嵌入其中。更一般地说，给定一个相容的素OMP，我们总是可以定义一个CE变迁系统（因此也是一个CE网系统），如下所示。定义3.1设P是一个相干的素数OMP。德费恩J（P）=（FP（P），EP，TP）其中，E P={f\g，g\f ff|f，g ∈ FP（P），fg}，且（f，e，g）∈ T Pi e=f\g，g\f.注意，不同的素滤波器对可以产生相同的事件;这意味着事件可以发生在不同的全局状态中，具有相同的局部效应。我们现在有两个映射：H将一个凝聚的素正交模偏序集与一个转移系统相关联;J则相反。在[1]中，它表明，J（P）属于由条件网和事件网生成的变迁系统（即CE变迁系统）。 在同一篇论文中，我们证明了对于所有CE迁移系统A，A嵌入JH（A），P嵌入HJ（P）。在这两种情况下，嵌入都是由态射的自然概念给出的。我们猜想H（A）和HJH（A）是同构的OMP，J（P）和JHJ（P）是同构的转移系统，但这些问题仍然是公开如果这两个假设成立，我们可以将HJ和JH解释为各自域中的一种一个相关的公开问题是通过区域的过渡系统生成的正交模偏序集的特征在下文中，我们描述了实现这一目标的一个步骤。定义3.2一个正交模偏序集P是区域的，如果它对于某个过渡系统A同构于H（A）。每个区域OMP都是一致的和素的;然而，也有不属于区域的一致的和素的OMP;下面的例子描述了一个简单的例子。例3.3设B ={1，.，6}且Ω ={X<${1，...，（六）||X|是偶数。很容易验证P =Ω，B，（. ）B是一个凝聚素正交模偏序集，其中的邻补是B的P有六个素滤波器;一个典型的素滤波器是由所有X∈Ω包含给定的i∈B的集合给出的。相应的转移系统J（P）有六个状态，并且所有的状态子集都是区域。因此，HJ（P）是具有六个原子的布尔代数，并且P嵌入到HJ（P）中。正如这个例子所示，相干和素OMP的类严格大于区域OMP的类。L. Bernardinello et al. /Electronic Notes in Theoretical Computer Science 270（1）（2011）147153在我们的搜索区域正交模偏序集的特征，我们寻找特殊的属性，可以在抽象的设置OMP翻译的具体地区。引理3.4设A是CE转移系统。 设x，y，z是A的区域，x<$y = y <$z= z <$x;则x <$y <$z是A的一个区域。这个引理的证明是一个例行的验证。对于OMP可以陈述类似的定义3.5设P是一个凝聚素OMP。如果下列性质成立，则称P为富[x]<$[y]= [y]<$[z]= [z]<$[x]<$$>w∈P：[w]= [x]<$[y]<$[z]请注意，例3.3中描述的OMP是连贯的和主要的，但不是丰富的，也不是区域性的。定理3.6各区域OMP丰富。证据设P为区域OMP。则存在CE转移系统A=（S，E，T）使得P同构于H（A）.在这个证明中，我们研究H（A）。设x，y，z ∈ R A使得[x]<$[y]=[y]<$[z]=[z]<$[x].我们已经说过，H（A）的素滤波器与A的态之间的对应不是双射的;更确切地说，可以存在不对应于A的态的H（A）的素滤波器。然后我们可以将素滤波器集合[x]分解为两个不相交的子集：[x]= X1<$X2，其中X1={f∈ [x] |f = fs ， 对 于 某 些 s ∈ S}， X2=[x]\X1. 以 类 似 的 方 式 ， 我 们 分 解[y]=Y1<$Y2，[z]=Z1<$Z2。则 X1<$Y1=Y1<$Z1=Z1<$X1 。 为 了 证 明 这 个 陈 述 ， 注 意 Y1<$X2=<$ ，Y2<$X1=<$ ， 因 此 [x]<$[y]= （ X1<$Y1 ） <$ （ X2<$Y2 ） ， 对 于 [y]<$[z] 和[x]<$[z]也是类似集合X1包含对应于A的状态的所有滤波器，并且包含x;我们可以用x将它标识为A的区域，因为状态和滤波器之间的对应是单射的。 然后，我们推导出x<$y=y<$z=z<$x ， 其 中 我 们 将 x ， y ， z 视 为 区 域 。 由 引 理 3.4 可 知 ，w=x<$y<$z是A的一个区域，也是H（A）的一个元素很容易证明，在任何正交模偏序集P中，对所有p，q∈P使得p$q成立[p]<$[q]= [p<$q] 。 在 H （ A ） 中 ， 我 们 有 w=x<$y ， 因 此 w=x<$y ， 所 以[w]=[x]<$[y]=[x]<$[y]<$[z]。Q它仍然是一个悬而未决的问题，是否所有连贯的，主要的，丰富的OMP是区域。在研究区域OMP的表征过程中，我们计划研究OMP各种性质之间的相互关系。特别地，我们知道一个OMP可以是丰富的和非素的（以一个没有素过滤器的OMP为例）;我们将研究丰富性和足够的素过滤器的存在是否意味着连贯性。154L. Bernardinello et al. /Electronic Notes in Theoretical Computer Science 270（1）（2011）1474由出现网我们已经证明，定义在CE的局部状态上的自然序关系 网系统产生一个正交模偏序集，当网系统是饱和的局部状态。从Petri网生成正交模偏序集的一种不同方法是建立在发生网的基础上。这些是条件和事件的非循环网，最初是作为并发进程的模型引入的;它们可以自然地用于定义一般CE网系统的语义，在网理论中表达Petri定义了一个具有规则结构的发生网，作为相对论时空的一种离散表示。这样就可以在网的元素子集上定义一个闭包系统，以及一个相应的正交补。闭子集形成一个正交模格;这个结果类似于几个作者（例如，见[2]）对通常的闵可夫斯基时空的结果，并提出了一个不同的研究方向。引用[1] L.贝尔纳迪内洛角Ferigato和L.波梅洛分布式系统中可观测特性的代数模型。理论计算机科学，290：637[2] W. Ceg-la和A.弗罗雷克Minkowski空间的因果逻辑C o m m u n . 数学Phys. ，57，1977。[3] A. Eschericht和G.罗森伯格偏（集）2-结构i ii。Acta Inform.，27（4）：315-368，1990.[4] C. A. 彼得我想和你一起去。InstitutfurInstrumentelleMathematik，SchriftendesIIM，2，1962.[5] C. A.佩特里网络理论的概念。计算机科学的数学基础，第137-146页，1973年。[6] C. A.佩特里物理学和计算中的状态转换结构。Journal of Theoretical Physics，21（12）：979[7] P. 普特阿克山口 普尔曼来了。 作为量子逻辑的正交结构。 Kl uwerAcademicPublishers，1991.