带计数器的无边界可达性图：带整数变量向量丰富的佩特里网的等价行为表示

《理论计算机科学电子笔记》239（2009）119-129www.elsevier.com/locate/entcs无边界计数器的有效可达性图表示弗兰克·波默罗1L ACL，Univer siteParis12. 61avenue d'ge n'eraldeGaulle. 94010Creteil，France雷蒙德·德维勒斯2在我的书中，我读到了一个很好的例子，我读到了一个很好的例子，我读到了一个很好的例子。CP212、B-1050Bruxe lles、Belgium汉娜·克劳德尔3IBISC，FRE2873CNRS，U n iveriteEvry-ValdE ssonn e. 91000Evry，France摘要在本文中，我们定义了一类名为带计数器的佩特里网，它可以被看作是用整数变量向量丰富的位置/转换佩特里网，可以在其上应用线性运算。它们的语义通常会导致巨大或无限的可达性图。然后，这种语义学的一个更紧凑的表示被定义为一个符号状态图，其中节点可能对变量的无限多个值进行编码。这两种表示在行为上是等价的。关键词：网、不限积分器、可达性、迹线。1引言处理（特别是模型检查）具有巨大或无限状态空间的系统通常是有问题的，特别是当必须管理具有无限多个值的数据时。例如，当包含有效的结构良好的系统时（其中的演化是单调的，尊重一些选择良好的准秩序），当被感知的状态集向上或向下闭合时，并且这些状态集可以由一组有限的生成器来表征时，这个问题可以解决。可达性集通常不会自行关闭，但在数据1电子邮件：franck. univ-paris12.fr2 电子邮件地址：rdevil@ulb.ac.be3电子邮件地址：klaudel@ibisc.univ-evry.fr1571-0661/© 2009爱思唯尔B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2009.05.034120F. Pommereau等人/理论计算机科学电子笔记239（2009）119DFDF空间是规则的，这通常是实践中的情况（即使在所有性别中，可达性往往是不可决定的），它可能发生，它可以使用有限的结构来表示。这意味着能够表示无限的状态集，并在一定时间内计算可能的无限的可达到状态集。例如，[1]中开发的方法（并在[2]中实现）允许精细数据结构表示可以在Presburger算术中完成的整数向量集，并将其应用于线性变换。它也允许在有限的时间内计算在[1]元转换中称为的无限序列变换的结果。如果可以执行足够的元转换，则可以在有限的时间内计算（和表示）系统的完整状态空间。当然，不是所有的状态空间都可以被赋予有限的表示，或者不是所有的元转换都可以使用有限的计算来执行。事实上，存在着不可能实现这种"浓缩"的变换，但正如本文的目的是将这些技术应用于佩特里网的背景下。为了做到这一点，我们定义了一类佩特里网，称为带计数器的佩特里网（PNZ）。它们是用整数变量的全局向量中的数据丰富的位置/转换（P/T）皮氏网，通过线性变换进行操作。PNZ中的点、弧和PNZ可以被理解为在其位置中编码控制状态，在其变量中编码数据状态。它也可以被看作是彩色皮氏网的一个特殊情况，它将整数变量简单地表示为整数标记的位置。它的语义通常导致产生无限的可达性图。一个更紧凑的状态图结构是由下一个完成的。这是通过检测更改数据状态但不更改控制状态的执行，并将其作为元转换执行来实现的。结果是一个紧凑的图，其中每个可能的状态编码了大量或无限数量的可达到标记。本文的主要结果是证明压缩状态图保留了系统的语义，因为它对完全相同的跟踪集（填充序列）和可达标记集进行了编码。特别引入一个配备压缩语义学的具有无限计数器的佩特里网模型的基本动机是希望使用因果时间方法来有效验证建模系统，其中时间的流逝通过计算滴答声转换的发生来显式表示[5]。2基本符号和定义让Z表示一组积分，D ={·}Z表示一组数据值，其中" · "是佩特里网黑令牌。 如果f和g是域H上的两个函数，我们用f g表示它们的合成，对于所有a奏效为（f g）（a）= f（g（a））。设n≥ 0为整数，设V={x0，...，x n−1}是一个有限的变量集，使得V Δ D = −。我们还将假定对这些变量进行了排序。F. Pommereau等人/理论计算机科学电子笔记239（2009）119121DF3DF并由X = [x0，...]减记[x n−1]>>枚举所有的对应向量这些变量。 在这些例子中，我们将使用X= [x，y，z]或简单地使用X=[x]。线性变换L是对（C，U），其中：• C是线性条件，即形式为PX≤Q的表达式，其中P是m×n整数矩阵，其中Q是Zm中的向量，对于m≥0;• U是线性更新，即形式为AX+B的表达式，其中A是n×n整数矩阵且B≤Zn。线性条件允许表达多种（合取）条件。例如，（x y）（x+ 2y = 3z）（z >5）等价于（x−y≤ −1）（x+ 2y− 3z≤ 0）（−x−2y + 3z≤ 0）（−z≤ −6），为线性。不一致的类型γ1γ2的条件，特别是类型a的条件b）事实上是什么（a−b≤ −1）λ（b−a≤ −1））是不可表达的，但它们可以被将每个不同的不一致性与同一更新相关联的几个线性变换所取代。线性更新允许同时分配X中的所有变量及其先前值的线性组合（因此禁止倍增变量）。例如，我们可能有（x：= 2x +y+3;y：=z;z：=y+ 1）。结合前面给出的线性条件，我们得到以下线性变换：02 3 2 31- 102 3−12B612−37 x6 0 7三二三二一2 1 0x3CB6 7 6y 7≤ 6 76 00 17 6y 7+ 60 7CB6 74 56 745 4 54 5C@4−1 −2 35Z0 0 0 -1405-6A01 0z1在下面的文章中，我们将使用矩阵或扩展公式。对于大小为n的向量V，我们用V[xi]表示它的第i个分量。在上面的例子中，线性更新U是U[x]=2x+y+3，U[y]=z和U[z]=y+1。设ZZn和L是线性变换（PX≤Q，AX+B）。L在Z上的应用，以L（Z）为单位，是以{ AY + B}为单位的Z n的子集|Y且Y≤Q}。 更重要的是，LonZ的迭代应用，由L*（Z），是集合（Z）ff的递增级数的极限（并）ii≥0，其中Z0=Z其中Zi+1=Zi=L（Zi）。2.1彩色皮氏网AColouredPetrinet（CPN）[4]onDandVisaupleN=df（S，T，l）whereSi是一个有限的地方集，T是一个有限的过渡集，其特征为SεT=λ，l是关于地方、过渡和弧的标记函数（元素来自（S×T）ω（T×S））：• 对于每个地方s奏效，l（s）D是s的类型;• 对于每个转换t≥T，l（t）是V上的可计算布尔表达式，称为t的保护（其执行的条件• 对于每个输入arc（s，t）≥S×T，l（s，t）是D−V上的有限多集，repres-发送在执行时消耗的值;• 对于每个输出arc（t，s）≥T×S，l（t，s）是D中的值、V中的变量或其上的可赋值表达式的有限多集，表示执行t时在s中产生的值。与输入案例的不同之处在于，允许使用表达式计算新值122F. Pommereau等人/理论计算机科学电子笔记239（2009）1190CPNN =（S，T，l）的状态由标记M表示，标记M是与每个位置s奏效的映射，标记M是l（s）上的多集M（s如果存在这样的约束ρ：V→D，则在M处启用转换t>T：• 警卫的评估为真：evalρ（l（t））=T;• 对于每个弧（s，t），在s处有足够的令牌：M（s）≥evalρ（l（s，t））;• 对于每个弧（t，s），s的类型是：evalρ（l（t，s））是l（s）上的有限多集。如果t在M处启用绑定ρ，则它可能会启动，导致新的标记MJ对于每个s}JDF-eval（l（s，t））+eval（l（t，s））MJ是当时S乘以M（s）=M（s）ρ ρ称为从M一步可达（注意，在一般情况下，许多不同的绑定可以从M到MJ到t）。一个痕迹，四个或一个燃烧序列，ngthk≥0ofamarkedCPN（N，M）issM−t−1−，−ρ−→−1 ··−t−k−，−ρ−→−k M，WHERE0 0K对于所有1≤i≤k，通过用绑定填充ti，可以在从Mi−1的一步内到达ρi.然后说Mk可以从M0到达（在k步中）;迹线k（N，M0）表示DF长度为k（N，M0）和Trace（N，M0）的所有迹线的集合=k≥0迹线k（N，M0）是（N，M）的所有迹的集合标记的F家族的一组痕迹DFCPN的定义为Trace（F）=（N，M0）>FTrace（N，M0）。从初始标记M0到N的标记的可达性可以表示为（可能是无限的）可达性图，该图是有向图，其中节点都是可达标记，并且每个弧表示从一个节点到另一个节点的转换和绑定。在这种情况下，可达性图可以被认为是迹线（N，M0）的紧凑表示。特别是，它可能仍然是有限的（即具有有限数量的可达到标记），即使它允许无限的痕迹。彩色皮氏网可以被看作是P/T网的推广，或者，另一方面，P/T网是受限的彩色皮氏网，其中：• 对于每个位置s奏效，l（s）={·};• 对于每个跃迁t≥T，l（t）=T（真防护）• 对于每个弧（a，b）奏效（S×T），l（a，b）是{·}上的有限多集。因为这样的网不使用任何变量，所以它的绑定是无关紧要的，将在下面被忽略。像往常一样，佩特里网将使用圆作为正方形，矩形作为过渡，有向链接作为弧以图形方式表示。将省略由空多集标记的弧，以及默认注释：T表示真正的保护和{·}表示空格类型或蝴蝶结标签。3带计数器带计数器的佩特里网（PNZ）是一个P/T网，其中的数据由整数值（计数器）的全局向量V≥Zn允许检查和更新的具有4痕迹不应与Mazurkiewicz的痕迹F. Pommereau等人/理论计算机科学电子笔记239（2009）119123VDFDFxL（a，b）=L（a，b）;x（x>0，x：=x− 1）（x ω/2，x：=x+1）t1S1T2·T3S2T4T5（x ω，x：=x+ 1）（x>0，x：=x− 1）（x ω，x：=x+ 1）F. I.G. 1. Anexam p l l e PNZ，forwhichwe ss um e X=[x];i tni ti a ldat a是D0={[0]}andachtran ioii i n由其关联的线性变换标记。参数ω是定常的非负整数。DF每个过渡结束时的数据。更准确地说，PNZ是一个元组N=DF（S，T，l，L）其中[N=（S，T，l）是P/T网，L是与每个P/T网相关联的映射。DFT中的过渡t是线性变换L（t）=（C（t），U（t））。PNZ示例为如图1所示PNZN的A（聚合）状态是对（M，D），其中M是[N]的标记和DZn，其中D是V的一组可能值。A状态（M，D）如此D是一个单例称为一个具体状态;一个一般编码为几个的具体的国家，可能无限多的。3.1NPC的CPN语义设N=（S，T，l，L），其中L=（C，U）在其上限定，是一个PNZ，（M，D）是它的我是一个男人。 Itcanbetranslatedintoa familycpn（N，D，D）=ff{（（SJ， TJ，lJ）， M）|仅因初始标记而不同的标记CPN（每个标记与特定初始状态相对应的标记），其中：• SJ=sfS{s}|x›V}andTJ=dfT;• foralls奏效，lJ（s）=pdf{·}andfo ralx奏效，lJ（s）=pdfZ;DF DF• 对于所有s物资，MV（s）=M（s），对于所有x物资，MV（sx）=V[x];• forallt÷T，lJ（t）=sfC（t）;• 对于所有（a，b）奏效（S×T）=（T× Jpdf• 对于所有t>T，对于所有x>V，lJ（s）x，t）={x}和lJ（t，sx）={U（t）[x]}。处于初始状态（M，D）的PNZN的语义是对应的翻译CPN的迹的集合迹（cpn（N，M，D））图2和图3分别示出了这样的翻译、给出单个CPN以及相应的可达性图的示例。为了比较PNZ的具体状态和CPN的标记M，我们将最后一个对（M·，V）去符号化，其中M·M被限制为placesoftype{·}andV÷Znis sdforeachx>V byV[x]=sfM（s）。F或Rx例如，图2中描述的NCP的标记可以表示为x ω/2sx0x+1xT1x−1xs1·124F. Pommereau等人/理论计算机科学电子笔记239（2009）119x>0T2xx+1s2t4x ωx+1xT3x ωxx−1T5x>0图2. 图1中PNZ的CPN翻译。F. Pommereau等人/理论计算机科学电子笔记239（2009）1191257：2;30：s1;012：2;6T1T2T3T1T4T2T3T1T4T2T3T5T4T3T2T5T5T4T3T2T5T5T4T4T3T5T2图3.图2中ω= 6时CPN的可达性图。每个状态都用它的编号、{s1，s2}中被标记的位置和sx的标记来标记。当ω增长时，图的左部分和右部分（通过状态6和7连接）在保持相同结构的同时变高。（1）（2）（3）（4）（5）（6）（7）（8）（9）（10）（11）（12）（13）（14）（15）（16）（17）（18）（19）注意，还可以首先将新变量vs与N的每个位置s相关联，在M（s）=m· {·}时将值m与vs相关联，为N的每个转换保持具有侧循环的单个位置，并适当地适应它们的线性变换。然而，净损益转换的筛选条件在这些新变量中是线性的，其筛选结果也是线性的。然而，通常最好保留原始位置，因为网络的控制状态具有直观的含义，并且在许多实际系统中，可达到的状态对应于这些位置的安全标记（在每个控制位置中最多一个）。3.2更紧凑的可达性图设N=（S，T，l，L）是处于初始状态（M0，D0）的PNZ。它的语义可以通过符号状态图以更紧凑的方式来捕获，其中节点是PNZ的状态，可能无限地聚合CPN中的许多CPN标记（N，M0，D0）。 更精确地说，如果在状态（M，D）处启用了转换t>T， 在M处启用t，并且在D处至少有一个向量满足条件C（t）。t的火产生一个状态（MJ，DJ），因此Mj是由在[N]中填充t按以下内容构建：和DDF=L（t）（D）。 因此，可以形成压缩状态图G。• （M0，D0）是G的节点。• 如果（M，D）是G的一个节点，使得（M，D）在N中转换t，并且（MJ，DJ）is tt atereachablfrom（M，D）bythefiingoft，then，forDJ=dfJ JJJJDFJL（t）（D）如果M=M，或者D=D，则我们有：· 如果在G中没有节点（MJ，Djj），则我们将节点（MJ，Djj）添加到G，并将标记为t的弧从（Mj，D）添加到（MJ，DJJ），· 或者，我们在G中选择任意节点（MJ，DJJ），即DjjDJJ并将由t标记的弧从（M，D）添加到（MJ，DJJJ）。直观地说，如果在（M，D）导致（M，DJ）时不能进行转换，则意味着JJ JJDF*Jt可以（可能多次）从（M，D）D=L（t）（D），至少如果C让它。因此，该想法是将获得的所有射击序列的效果汇总1：1;13：s1;29：1;46：2;25：1;311：1;58：2;44：2;113：1;62：s2;010：2;5J126F. Pommereau等人/理论计算机科学电子笔记239（2009）1194：2; 0，...和ω-13：2; 1，... 和ω2：s2;x≥ 01：s1;x≥ 1DFKKT5T2T3T1T1T4T4T2T3T1T1T5T5T4T2T36：1; 1，... 和ω图4.当6 ≤ω<∞时，图1中PNZ的压缩态图 每个状态由其在构造中的排名、标记的位置（eithers1或s2）和x的可能值集来标记。 注意，如果在5之前构建了6，则节点5可能指向6而不是T1T5T1T2T4T3图5。当ω为无穷大时，图1中PNZ的状态图，即当所有涉及ω的条件都被丢弃时。迭代t（它们可能是无限的），被认为是元转换，进入一个符号状态（M，DJJ）。由于L（t）*的应用，当计算（M，DJJ）的后继者时，总是构造由t标记的（M，DJJ）上的循环弧。另一方面，如果从（M，D）计算的状态是（MJ，DJJ），并且具有DjjDJJJ的状态（MJ，DJJJ）已经存在于G中，则（MJ，DJJ）被（MJ，DJJ）覆盖并且不需要被添加。也可能发生的是，一个计算态覆盖了G中已经存在的一些态（当DjjjDJJ）。这将在第5节中讨论。应该注意的是，这种构造并不保证G是唯一的（甚至是有限的）;它还可能取决于在哪些节点和转换中被考虑得很好，以及在哪些节点和转换中选择了DJJJ（当可能有多个节点时）。然而，这将对所需属性没有影响我们用G（N，M0，D0）表示denote上面构建的任何可能的图形。这种状态图的示例如图4和图5所示。由于图G=G（N，M0，D0）中的状态可以聚合多个具体状态，因此从（M0，D0）开始的路径实际上可以编码多个基本路径。(We稍后将显示这些基本路径实际上与PNZ的轨迹相对应更精确地说，对于k≥0，让Pk（G）是长度为k的所有路径的集合DFT1TKGthatt ta t trtat（M0，D0）。 Then，ifπ=（M0，D0）（M，D）isapathinPk（G）（如果k = 0，则可能还原为初始状态），然后我们将其展开的unf（π）定义为由π表示的长度为k的所有基本路径的集合，即实际上可能发生的具体状态之间的转换序列。更多精确地，unf（π）包括所有基本路径（M，V）t1TK （M，V）0 0 -→ ·· -→ kk kf orallVi壮大Di（0≤i≤k）andsuchthatL（tj）（Vj−1）=Vj（for1≤j≤k）。THES和DF长度为k的基本路径由路径k（G）=π奏效Pk（G）unf（π）给出。 一套零长度基本路径是路径0（G）={（M0，V）|V次方D0}。 最后，G的一组基本路径（我们也称之为PNZ基本路径）DF设为路径（G）=k≥0路径k（G）。1：1，1，...ω/20：s1;05：1; 2，... 和ω0：s1;02：2; 0，... ω/2 − 1F. Pommereau等人/理论计算机科学电子笔记239（2009）119127KKkDF应该注意的是，在压缩状态图中可能存在不对应于任何基本路径的路径，即，实际上无法执行。Tisithecasefo rintthegraphof thfigure5当er t he e path0−t−1−→1−t−2−→2−t−5−→2isunfoldddtoanemp tys et（aftert1，t2wehavex=0thust5isdis abled）。4行为等效性DFA PNZ基本路径π=（M0，V0）t1-→··tk−→（M，V）isequivaenttoaCPNdftJ，ρ1tJ，ρktraceπJ=（MJ， VJ）−1−→−·· ·−→−（MJ， VJ）ofthesamelngthk，denotedπ~πJ，0 0 k kk如果对于0≤i≤k，MJ =Mi，VJ=Vi且ti=tJ。PNZ基本路径的集合我是我等价于一组CPN迹，记为πJ，如果存在双射因此，对于所有的p，p是这样的。定理4.1让N成为处于（M，D）状态的PNZ。对 于 任何状态图。G= G（N，M，D），我们有路径（G）~轨迹（cpn（N，M，D））。通过在基本路径的长度上进行归纳来证明这一点，DF痕迹。设NZ是初始状态（M0，D0）下的PNZ，G=G（NZ，M0，D0）NZ的任意状态图在不损失一般性的情况下，我们假设D0是单例{V0}。然后，cpn（NZ，M0，D0）={（NC，（M0，V0））}。根据cpn的定义，NZ和NC具有相同的跃迁集基本案例：k= 0。 根据定义，我们有路径0（G）={（M0，V）|VεD0}={（M0，V0）}=迹线0（NC，（M0，V0））。归纳假说。假设路径i（G）~ tracei（NC，（M0，V0）），对于所有i，如0 ≤i≤ k。诱导步骤：k +1。值得注意的是，在一条轨道上（M，V）t1，ρ1tk，ρk0 0 -→- ···→→→（Mk，Vk）对于一个CPN，绑定ρ i完全由Vi −1对于1 ≤ i≤k确定：根据cpn的定义，特别是如何设置弧，我们必须有ρ i={x›→V i−1 [x]|x>V。因此，我们将不考虑以下链接。（vi）让πDF （M，V）t1=tktk+1（M、V）（M）（V）成为一个元素-0 0 -→ ·· -→ kkk→→→k+1k+1路径k+1（G）中的路径。 根据归纳假设，我们有一条唯一的迹线（M0，V0）−t−1−，−ρ−→−1 ·· −t−k−，−ρ−→−k（M， V）intrace（N， V）thatsequivalnttttt t hefixK K K C0 0π的（M，V）t1tk（M，V）。 根据CPN的定义，特别是如何守卫0 0 -→ ·· -→ kk k和弧的地方x（M、V）JDFt1，ρ1tk，ρktk+1，ρk+1（M、V）（M）（五 ）k+1k+1）。 因此，π=（M0，V0）→→→ ···-K-KK+1k+1是迹k+1（NC，M0，V0）中的迹，它是唯一的且πJ。（）这可能主要由对称论证来证明。Q4.1可达性等同性根据定理4.1，一个状态图被允许编码比实际可到达标记更多的内容;然而，由于展开，只保留了可执行的基本路径。我们现在表明，状态图精确地包含当前可到达的状态，每个这样的状态通常仅通过图中导致它的路径的子集可到达。128F. Pommereau等人/理论计算机科学电子笔记239（2009）119A BT1T2MJ，DJJT3T4T5C. F.ET7T2T1T6MJ、DJ......=⇒图6.左：添加（MJ，DJJ）并覆盖（MJ，DJJ）。中间：A和B连接到新状态右：（M j，D jj）被删除，然后C变得不可访问，也被删除。推论4.2设N是一个状态为（M0，D0）的PNZ和一个相应的压缩状态图G。对于G中的所有节点（M，D）和D中的所有V，存在一个标记网（N J，（M J，V J））> cpn（N，M0，D0），使得（M，V）可以从（M J，VJ）在N j中到达。相反，对于所有有标记的网（N J，（M J，V J））> cpn（N，M0，D0）和所有（M，V）可从（M J，V J）在N j中到达，在G中存在这样的节点（M J，DJ），即VJ>DJ。（）通过G的构造保持：它只创建实际上从初始一个通过有限（但可能迭代）的转换序列到达的状态。根据定理4.1，等价执行导致等价状态。 Q5实施问题我们已经制作了一个原型实现，可以计算PNZ的压缩状态图。使用[1]中定义的NDD结构存储整数向量集，并在Lash库[2]中实现在某些情况下，当Lash无法迭代转换时，我们的简单化会以错误结束（正如引言中所解释的，这种方法并不完整）。此外，我们不能保证它会结束，因为这是一个一般无法决定的问题。然而，在[1]中已经给出了足够的终止条件，并且作为未来的工作来研究它们如何在我们的设置中应用。我们还根据上面给出的定义实施了优化。如果一个现有的状态被一个新计算的状态所覆盖，则前一个状态可以被后来的人取代这意味着被取代者的继承人必须被重新考虑，就像他们自己的继承人一样，因此。让（MJ，DJJ）成为新的状态，（MJ，DJJ）成为DjjDJJ这样的存在者。对于每个状态（M，D），其是（MJ，DJJ）通过由t标记的弧的前体，我们创建从（M，D）到（MJ，DJJ）的弧，也由t标记。然后，（MJ，DJJJ）被删除，作为以及从初始节点变得不可访问的所有后续节点，因此如图6所示。通过这样做，我们实现了两个预期目标：（MJ，DJJ）被（MJ，DJJ）他的继任者将被重新任命。然而，在图6中，由于C已经被移除，当计算（MJ，DJJ）的后继时，将产生其的推广。这也适用于F，但不能删除，因为它有一个前身E。如果我们后来发现F的推广是（MJ，DJJ）的后继，AT1MJ，DJJBT2T3T4T5C. FT6..ET7MJ、DJA BT1FT6.ET7T2MJ、DJF. Pommereau等人/理论计算机科学电子笔记239（2009）119129T5T4T33：2; 1，... 和ω5：2; 0，...和ω-16：1; 1，...和ω121216 4 2 65DFT4T1T1T3T5T2图7.删除覆盖状态后的状态图：根据图4中的图，状态1和4已被删除，因为它们被状态6覆盖，状态2已被删除，因为它被状态5覆盖。这个新节点将替换F，E将连接到它，就像刚刚显示的那样。我们还引入了另一个优化：由于（Mj，DJJ）概括了（MJ，DJJ），从（MJ，Djj）到（MJ，DJJ）的任何执行都可以一次又一次地执行：我们在状态图中发现了一个循环。因此，我们可以迭代从DJJJ创建DJJ的变换。在我们的例子中，我们得到DJJ作为L（DJJ）andalsoasL（DJJ），where5L=pdfL（t）L（t）andL=pdfL（t）L（t）L（t3），因为存在从（MJ，DJJ）到（MJ，DJJ）的两条路径。因此，可以执行对应于应用于DJJ的L1或L2或其任何组合的迭代的元转换。不幸的是，我们不能使用（L1← L2）*，这是一个不可用的线性变换运算。在我们的实现中，我们计算组合L= LL，并在替换（MJ，DJJ）时考虑L *（Djj）而不是Djj。这不是唯一的解决方案，但有一个无限的数字L1和L2的可能组合，因此我们选择考虑其中之一。这种优化的性质应该在未来进行研究应该强调的是，这些优化不会改变基本路径ENCODEBYTHEGRAPH. 印度eed，al llthellmentarpathsbasedonA−t−1−→（MJ，DJ JJ）arnowencod d ddbyA−t−1−→（MJ，DJJ）. EvenifDJJhasmorevallthanDJJ实际上可以从A计算的值将用于基本路径。更重要的是，很明显，优化对可达性没有影响。作为这些优化的结果，我们得到图7所示的图。6结论在这里，我们提出了一类带计数器的佩特里网（PNZ），作为P/T网，富含可以应用线性运算的无界（两端）整数变量。PNZ的语义是由一系列彩色佩特里网提供的，这些网将整数变量简单地表示为整数标记的位置。我们提出了一个紧凑的状态图构造，允许将许多可达到的标记（可能是无限多个）聚合到单个状态中。该图已被证明可以保留跟踪语义并准确地编码可达标记集。最后，我们引入了优化，以产生甚至更紧凑的状态图。我们的下一步将是一系列的案例研究，以证明即使不是完整的，这种方法在实践中也是有用和有效的;特别是对于具有有限但大的状态空间的系统。我们的第一个实验表明，这是具有因果时间的网络的情况，即使我们认为它是无限的。请注意，当我们进行链线性变换时，我们不仅要编写它们的更新，还要编写它们的条件;幸运的是，两者都是线性的。0：s1;0130F. Pommereau等人/理论计算机科学电子笔记239（2009）119计数器。未来的工程应该研究施工的完成问题，这与知道状态图是否完成直接相关。此外，我们应该仔细研究第5节中引入的优化，该优化在状态图中发现循环时执行元转换。由于定理4.1与所考虑的状态图G的选择无关，因此在构造G的过程中，也有可能使用导致更小图的适当条件另一个有趣的工作将是将我们的方法推广到[1]中定义的其他数据结构：Rn的子集和积分器的无界FIFO队列。参考文献[1] B. Boigelot. 如果你不知道，我就不知道该怎么办了。 P HDTHES，U NI V. 1999年，任中共中央政治局委员。[2] B.Boigelot.我的意思是，我的意思是。http://www.montefiore.ulg.ac.be/~boigelot/research/lash/[3] G. Geeraerts。结构良好的跃迁系统的覆盖性和表现性。2007年，任中共中央政治局委员、书记处书记。[4] K. 詹森。彩色皮氏网。基本概念、分析方法和实际使用。EATCS理论计算机科学专著，1.施普林格，1992年。[5] F.波默罗。 因果时间演算。 表格[6] W. Reisig. 培养网。EATCS理论计算机科学专著。施普林格，1985年。