理论计算机科学电子笔记144（2006）59-77www.elsevier.com/locate/entcs用秒表计算Petri网精确状态空间的一种摩根·马格宁1号IRCCyN，南特，法国迪迪埃·莱姆2奥尔堡大学-CISS，丹麦Olivier（H.）Roux3IRCCyN，南特，法国摘要在本文中，我们解决的问题的形式化验证的实时系统的优先调度策略的背景下。 我们提出了一个算法，计算的状态空间，该系统，建模为一个时间Petri网与秒表，准确和有效地，通过使用不同的边界矩阵（DBM），只要有可能，并自动切换到更多的时间和内存消耗的一般（凸）多面体只有当需要时。提出了一般多面体需要的一个充要条件。我们给出的实验结果比较我们的实施的方法，一个完整的DBM过近似和精确的计算，只有一般多面体。保留字：实时系统，时间Petri网，多面体1引言随着要求正确性证明的系统复杂性的增加，我们可能需要考虑涉及可以用1电子邮件：Morgan. irccyn.ec-nantes.fr2电子邮件：didier@cs.aau.dk3电子邮件：Olivier-h. irccyn.ec-nantes.fr1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.01.005M. Magnin等人理论计算机科学电子笔记144（2006）5960记忆他们的现状。一个明显的应用是在多任务环境中的抢占建模。这种暂停的概念需要引入变量，这些变量的连续演变可能会停止一段时间，然后在同一点恢复。 这导致了延伸 传统的时钟变量用“秒表”表示对形式模型的性质验证涉及到对它的部分或全部可达状态集的研究：它的状态空间。由于考虑了密集时间语义，这个状态空间通常是无限的。作为一个结果，验证算法计算它的有限抽象，保留待验证的属性在这些抽象中，具体的状态被编码成由离散部分（位置或标记）和连续部分（时钟/秒表的值）描述的状态的符号集连续部分用凸多面体表示，也就是说，用一组线性不等式表示。在具有简单时钟的模型（时间自动机，时间Petri网）的情况下，所考虑的多面体具有退化形式，可以将其编码为称为Difference BoundMatrix（DBM [4，8]）的有效数据结构处理DBM比处理一般的多面体要有效得多在处理秒表时，多面体保留了它们的一般形式，不能编码到DBMs中[14，17]：stowatch的表现力的增益被不可判定性结果[11，3]，验证算法的复杂性增加以及更高的内存消耗所平衡。针对与处理一般多面体相关的高复杂性和不可判定性结果的自然对策包括通过用更简单的包容多面体近似多面体来过度近似计算的状态空间，例如最紧密的包容DBM，其产生良好的计算加速[14，5，3]。然而，通过过近似保留的属性仅限于安全性：检查系统是否满足给定的直观的原因是，系统的实际行为包含在过度近似的行为中。此外，在DBM过度近似的情况下，在计算中要考虑的DBM的数量是有限的，这对于一般的多面体不一定是真因此，这可能使过度近似计算终止，而精确计算则不会终止。为了以有效的方式执行精确的分析，最近的工作使用过近似作为预计算，然后通过用网络的时间约束来限制结果以使其精确：在[5]中，作者对预计算的M. Magnin等人理论计算机科学电子笔记144（2006）5961使用DBM的全肠外营养。然后，给定一个来自过近似状态类图的无时间转移序列，他们可以获得序列转移之间的时间间隔，作为线性规划问题的解决方案。特别地，如果没有解，则过渡序列已经由过近似引入并且可以被清理，否则解集允许检查关于过渡的触发时间的定时属性在[15]中，作者将调度-TPN转换为秒表自动机，并使用HY TECH[10]进行后续验证。翻译使用DBM过近似来获得自动机的离散结构。然后，他们计算警卫和不变量的synn- tactically从网络的时间约束因此，离散的位置，可能被添加的过近似是不可达的，所得到的秒表自动机被证明是时间双相似的初始调度-TPN。这直观地意味着它的行为与调度-TPN的行为相同（而不是过度近似）。然而，这两种方法中使用的过度近似可能会导致它们不会通过向模型添加大量错误行为而终止，而精确计算将终止。换句话说，过度近似计算了无限多不可达的标记，而网络确实是有界的。本文提出的方法还解决了TPN秒表扩展的精确和高效的状态空间计算问题。它特别适用于抢占式TPN和调度式TPN。然而，为了简单起见，它是在调度-TPN模型上解释的。我们的做法基于以下两点：(i) 调度TPN的初始符号状态总是可以由DBM表示，(ii) 确定给定多面体是否是DBM是通过将[5]中给出的检测是否需要一般多面体的必要条件扩展为一个充分必要条件，我们能够提出一种混合的状态空间精确计算，它既使用有效的DBM表示，又仅在需要时使用一般多面体表示。我们已经实现了调度TPN的方法，并通过实验结果说明了它的有效性。本文的组织如下：第2节给出了调度-TPN模型的形式化定义，并说明了状态类图计算。第三节介绍了多面体计算的定理和证明第4节描述了一种算法，提高了精确状态空间计算的效率最后，在第5节中，我们简要介绍了该工具M. Magnin等人理论计算机科学电子笔记144（2006）5962··0P1，γ= 1，ω= 1P3，γ= 1，ω= 2t1[2， 3]t3[1， 4]P2，γ= 1，ω= 1P4，γ= 1，ω= 2t2[1， 2]t4[3， 5]图1.一、调度- 一个处理器上两个任务的算法的实现和一些实验结果。2调度时间Petri网2.1调度的定义和语义-TPN在[16]中，ROUX等人介绍了TPN对调度的扩展这扩展包括丰富的时间Petri网模型与调度策略（即，系统的不同处理器激活或暂停任务的方式）。定义2.1时间Petri网（TPN）是一个n元组T=（P，T，·（），·，α，β，M，Act），其中：• P ={p1，p2，.，pm}是一个非空的有限位置集。• T ={t1，t2，.，tn}是一个非空的有限变迁集（TP =）。•·（）：T→（NP）是后向关联函数。• （）·：T→（NP）是前向入射函数。•M0∈NP是网的初始标号• α∈（Q+）T和β∈（Q+∞}）T是分别给出每个跃迁的最早和最晚点火时间的函数（α≤β）。• Act∈（NP）NP是一个连续的标记函数. Act（M）表示标记M对调度策略的解释。Act是将TPN扩展为Scheduling-TPN的特定元素。例2.2图1给出了一个替代TPN的例子。网络的初始标记是{P1，P3}。但是，由于这两个位置被分配给同一个处理器，并且P3的优先级最高，因此初始活动标记为{P3}。因此，第一个触发的转换将是T3。网的一个标记M是NP的一个元素，使得P∈P，M（p）是位置p上的标记数。网的一个有效标记Act（M）是NP的一个元素，使得NP∈P：（）M. Magnin等人理论计算机科学电子笔记144（2006）5963• 如果与地点p相关联的任务当前被挂起，则Act（M（p））= 0• Act（M（p））=M（p）否则。在[16]中，Act（M）被定义为固定优先级调度策略;引入了三个新参数来处理这个模型：• Proc{φ，proc1，proc2，. proc1}是处理器的有限集合（包括被引入以指定不向硬件架构的有效处理器分 配 位 置 的φ），• ω∈NP是优先级分配函数。• γ∈ProcP是分配函数。实际上，当一个位置p并不代表处理器的真实活动（例如寄存器或内存状态）时，处理器（γ）和优先级（ω）都不必附加到它上面。这意味着对于这样的位置，我们总是有Act（M（p））=M（p）如果转换t由活动标记Act（M ）使能，则称其为活动的。我们用t∈enabled（Act（M））表示它。启用但未激活的转换称为挂起。设M是网的一个标记，并且是可量化的转移。我们用↑enabled（M，ti）表示触发ti后新启用的转换集，即，新标记M-·ti+ti·使能而不是M-·ti使能(ifti在其触发之后保持启用，则其被认为是新启用的）。从形式上讲，↑enabled（M，ti）={tk∈T|（·tk≤M−·ti+ ti·）<$（（tk= ti）<$（·tk>M−·ti））}类似地，我们将用disabled（M）表示由ti触发而禁用的转换集，即由M启用但不由M−·ti启用的转换。赋值是一个映射ν∈（R+）T，使得τt∈T，ν（t）是自上次启用t注意，只有当t是一个使能的转换时，ν（t）才有意义。0是空赋值，使得k，0k = 0。我们可以将调度扩展时间Petri网的语义定义为时间转移系统（TTS）[13]。在这个模型中，可能会发生两种类型的过渡：当时间流逝时的连续过渡和当网络发生过渡时的离散过渡。定义2.3一个转换TPNT的语义被定义为一个TTSST=（Q，q0，→），使得• Q=NP×（R+）T表示系统• q0=（M0，0）是初始状态• →∈Q×（T<$R）×Q是包含一个连续M. Magnin等人理论计算机科学电子笔记144（2006）5964¨⎪⎪转换关系和离散转换关系。·连续转移关系定义为：（M，ν）−→d⎧⎪⎪（M，νJ）iJ¨¨（i）ifAct（M）<·tM ≥·（t）如果ti∈enabled（M）， 则 v（ti）=？⎪拉克莱特 ∈T，M≥·t<$v（ti）+d否则，vJ（t）≤β（t）k k k k·离散的关系定义为i∈Tby：⎧ΔACT（M）≥·ti，⎪MJ=M−⎨·ti+ti·，（M，ν）−t→i（MJ，νJ）iα（t）≤ν（t）≤β（t），我爱你⎪¨如果tk∈↑enabled（M，ti），tk，ν（tk）=<$⎪¨（tk）否则2.2基于状态空间抽象的并行TPN算法2.2.1状态类图用于存储-TPN。为了分析时间Petri网，需要计算其可达状态空间。然而，时间Petri网的可达状态空间显然是无限的：Berthomieu和Diaz [2]提出了一种方法，将其划分为无限状态类的有限集合。在[14]中，LIME和ROUX推广了这种方法，给出了一个计算调度TPN状态空间的半算法（如[16]所证明的，调度TPN的可达性和有界性问题是不可判定的）。证明了时间Petri网类的激发域为θi−θj≤γij和αk≤θk≤βk的形式，其中i，j∈ {1，. n}，k∈{1，.，m}和γij，αk（和βk）是取决于i，j和k的整数常数。θi表示与转变ti相关联的时间估值。调度的状态类-TPN仍然被定义为具有标记和触发域的一对。然而，由于秒表的存在（这里是时钟的估值），状态类的触发域不能再编码到DBM中;需要一个一般的多面体形式定理2.4调度-TPN的状态类C是一对（M，D），其中M是网的一个标号，D是一组不等式。对于调度-TPN，域D的一般形式是具有m个约束的（凸）多面体我我⎪⎪⎩M. Magnin等人理论计算机科学电子笔记144（2006）5965FJ我我（m∈N）涉及多达n个变量，其中n是由类的标记Aθ≤B其中A和B是各自维度（m，n）的有理矩阵，并且（m，1），θ是n维向量在TPN的情况下，发射域比一般的多面体更简单，因此可以编码到有效的DBM数据结构中[4，8]）。我们需要一个新的定义，来定义从一个类到一个带有秒表的时间Petri网定义2.5[Fireability]设C=（M，D）是调度- TPN的状态类。一个变迁ti被称为可从Ci触发，则存在解（θ，.. . ，θ θ∈[0. n−1]−{i}，s. t. tj是活动的，θ∈≤θ∈。0n−1i j现在，给定类C=（M，D）和可固定转移tf，类CJ=（MJ，DJ）通过t的发射从C获得 由下式给出• MJ=M−·tf+tf·• 按照以下步骤计算DJ，并在下面标记为（D，tf）(i) 对于所有激活的转换的变量替换tj：θj=θf+θJ，(ii) 与正实数或零实数集R+的交集：θi，θJ≥0，(iii) 消除（例如使用Fourier-Motzkin方法[7]）所有变量，相对于由Tf的触发禁用的转换的表，(iv) 增加与新启用的转换相关的不等式阿勒特 ↑ ∈enabled（M，t），α（t）≤θJ≤β（t）.kfkkk每个多面体都有一个极小表示[1]。然而，在最坏的情况下，一般多面体的最小化的复杂性是指数的，而对于DBM，包含检验、相等检验和包含检验的复杂性是多项式的（O（n2），其中n是变量的个数），空检验和最小化的复杂性是O（n3）.变量替换对应于启用的转换：新原点对应于tf的触发时间。约束条件θJ≥0也可以写成θi≥θf，它表达了我们选择发射的事实tf，这意味着所有其他启用的转换稍后触发触发域不能总是用DBM表示的事实实际上意味着，例如，一个类可能具有以下域：{0≤θ1≤3 ， 0≤θ2≤4 ，0≤θ3≤4 ，1≤θ2+θ3≤7}（ 1）M. Magnin等人理论计算机科学电子笔记144（2006）5966·互斥···第33章[20、 28]t13[10，20]t21[100，∞]t31[150，150t11[50，50]P21，γ=1，ω= 2P31，γ=1，ω= 1P11，γ=1，ω= 2[18， 28]t32[0，0]t12[0，0]P32，γ=1，ω= 1P12，γ=1，ω= 2图二. 调度-TPN的两个周期性（与互斥信号量）和一个零星的进程我们在这里可以看到的是，最后两个不等式不能用DBM表示。此外，我们可以很容易地看到，这些新的不等式可能会给出更复杂的不等式（即涉及更多的变量），当触发另一个转换的域。2.2.2DBM过逼近处理一般的多面体比DBM消耗更多的时间和内存[1]。为了能够保持这些算法对时间表的效率ing-主题方案网络，李梅 等人 提出了一个过度近似的状态类用DBM [14]绘制了这类模型的图形该方法包括在包含它的DBM中包装多面体这可以通过下面的示例来说明：DBM过度近似包括写作，即激发域可以通过以下方式近似：、0≤θ1≤ 3， 0≤θ2≤ 4， 0≤θ3≤ 4（2）这种过度近似有一个明显的缺点：它可能会在状态类图中添加不应该到达的状态。此外，状态类图可以通过这种DBM-over-approximation变得无限，而确切的状态类图是有限的。图2的网络（[5]中提出的第二个例子）说明了这一点：只要我们不增加任务1的执行时间，DBM-over-approximately状态类图就保持有界（t13）。如果它增加到[10，23]，则DBM近似状态类图变得无界，而精确状态类图仍然是有限的。M. Magnin等人理论计算机科学电子笔记144（2006）5967···P1，γ= 1，ω= 1P2P4，γ= 1，ω= 2t1[4，5]t2[2，2]t4[1，1]P3t3[1，2]图三.第一个反例3约束可解的充要条件如前所述，带秒表的TPN的状态类图的特殊性在于出现了一些非DBM多面体形式一个主要的问题是，然后确定一个先验时，这样的多面体状态出现在状态类图的调度-TPN，我们研究。通过类中的DBM过近似来放松约束的一个条件如下：命题3.1父类包括挂起的和活动的转换，它们在导致当前类的转换的触发之前、期间和之后持续启用。在[5]中，这个条件被认为是必要和充分的。这个条件确实是必要的，但并不足够，因为我们现在将通过给出反例来证明它让我们来研究图3的网。在初始类中，有一个挂起的转换（t1）和一个活动的转换（t2），它们在t4的触发之后是持久的。在初始类中，t4是唯一可触发的转换。然后，它导致以下类：{{P1，P2}，{1≤θ1≤ 5，θ2 = 1}}这样一个类的触发域可以表示为DBM。然后，它遵循的条件是不够的，以确定何时计算的多面体将不是DBM。事实上，条件3.1需要对触发域中的转换时间进行一些额外的约束，以使其相关。这可以通过图4的网络来说明。在触发t2之后，有一个挂起的转换（t1）和一个活动的转换（t3），它们在触发t4之后是持久的。的解雇。M. Magnin等人理论计算机科学电子笔记144（2006）5968··P1，γ= 1，ω= 1P2P4t1[4，5]t2[1，1]t4[2， 4]P3，γ= 1，ω= 2t3[1， 2]见图4。 第二个反例t4导致以下类：{{P1，P3}，{3≤θ1≤ 4，0≤θ3≤ 1}}这样的类的激发域可以用DBM表示然而，如果与转换t2相关联的触发间隔减小到[0; 1]，则触发序列t2.t4导致：{{P1，P3}，{3≤θ1，0≤θ3≤ 1，θ1 +θ3≤ 5}}我们只通过改变跃迁的发射间隔t2就可以使非DBM多面体形式出现，这明确地表明条件3.1不足以定义过近似放松约束的情况。定理3.2（等效过逼近）设C =（M，D）是调度-TPN状态类，使得D是DBM（D={αi≤θi≤βi，θi-θj≤γij}是正则域）.设tf为aJ J J从C开始的可触发跃迁：t f的触发导致C =（M，D）。 设DJ为从D j得到的DBM-过近似域。DJ放松了D的约束（即域DJ不能仅用DBM表示;它的表示需要使用一般多面体）i <$i∈enabled（Act（M）），<$j ∈ enabled（M）−enabled（Act（M）），<$k ∈ enabled（M）−disabled（M，tf），s.t.. i/=k且βj+γki> βk+γji<$αj−γik<αk−γij证据设CJ=（MJ，DJ）是该调度TPN的状态类。设C=（M，D）是它的父类。对于这个演示，我们考虑一个有4个变量的域，但证明可以很容易地扩展到n个变量。使能的转换t1、t2、t3和t4与变量θ1、θ2、θ3和θ4相关联。 我们假设t1，t2和t3是活动的，而t4不是。最后，我们假设t1是可触发的，在C类中触发t1导致CJ类，并且t2在CJ中保持启用。·M. Magnin等人理论计算机科学电子笔记144（2006）5969⎨⎪J⎪⎪3初始域D的标准形式可以写成：⎧α1≤θ1≤β1，α2≤θ2≤β2，⎪⎪α3≤θ3≤β3，α4≤θ4≤β4，D=−γ21≤θ1−θ2≤γ12，−γ31≤θ1−θ3≤γ13，⎪<$−γ41≤θ1−θ4≤γ14，−γ32≤θ2−θ3≤γ23，⎪（三）⎪⎩42 ≤θ2 -θ4≤γ24 ，−γ43≤θ3 -θ4≤γ34现在，我们假设这四个不等式中至少有一个满足：β2+γ41<β4+γ21α4−γ12<α2−γ14β2+γ43<β4+γ23α4−γ32<α2−γ34让我们通过触发t1来计算从D获得的域DJ：我们开始于进行变量替换θ←θJ+θ对于所有活动转换，除了ii1所示的传输T1。我们在等式中定义了θ j，θJ≥0。 然后我们写为了使用Fourier-Motzkin方法，新的不等式⎧α1≤θ1，θ1≤β1，⎪jJ<$α2−θ2≤θ1，θ1≤β2−θ2，jJ<$α3−θ3≤θ1，θ1≤β3−θ3，⎪<$−γ41+θ4，≤θ1θ1≤γ14+θ4，⎪jJ<$−γ42+θ4−θ2≤θ1，θ1≤γ24+θ4−θ2，jJ（四）<$−γ43+θ4−θ3≤θ1，θ1≤γ34+θ4−θ3，⎪<$α4≤θJ≤β4，θJ≥0，⎪4 2⎪−γ32 ≤θJ−θJ ≤γ23，θJ≥0，⎪2 3 3⎪<$−γ21 ≤ −θJ ≤γ12，⎪2⎪−γ31≤ −θJ≤γ13傅里叶-莫茨金方法则包括写系统有解当且仅当θ1的下界小于或等于上界。然后，我们可以从前面的域推导出以下列表：−γM. Magnin等人理论计算机科学电子笔记144（2006）5970⎪⎪2222232约束：约束max{ 0，−γ12}≤θJ ≤γ21，⎪2拉吉max{ 0，−γ13}≤θ3≤γ31，⎪α4≤θ4 ≤β4，⎪jJ<$−γ32≤θ2−θ3≤γ23，θj−γ42−β1≤θJ−θ4≤γ24−α1，⎪− γ− β ≤θJ −θ ≤γ−α（五）⎪43 134⎪34 1<$α2−γ14≤θJ+θ4≤β2+γ41，⎪2⎪<$α3−γ14≤θJ+θ4≤β3+γ41，⎪3⎪<$α2−γ34≤θJ+θ4 −θJ≤β2+γ43，⎪2 3⎪<$α3−γ24≤θJ+θ4 −θJ≤β3+γ423 2我们可以注意到最后四行的所有非DBM约束至少使用了一个在C中活动的转换（t2或t3）和一个挂起的转换（t4）。因此，前面的必要条件的证明是直接的：在触发t1之后，如果类CJ不包含至少一个在C中活动的转移和一个不活动的转移，则不存在非DBM多面体形式在CJ的发射域。然而，人们应该注意到倒数是假的：让我们假设，例如，γ24=β2-α4和γ41=β4-α1（即这些约束在D中是多余的，这是我们从初始类开始的情况），那么不等式θJ+θ4≤β2+γ41可以通过com-比宁θJ≤γ21和θ4≤β4。 然后它是多余的，我们可以继续在其他约束也是如此特别是，这意味着不可能当从初始类开始触发转换时，从获得非DBM多面体我们现在要证明的是，在我们之前得到的四个多面体约束中，至少有一个与约束关于θJ+θ4，我们可以从对θJ的各个约束中推导出θ4（我们对θJ+θ4上的不等式不感兴趣，因为t3可能在触发t1后被禁用），这意味着：⎧<$α4+ max{ 0，−γ12}≤θJ +θ4≤β4+γ21，jJ（六）α4−γ32≤θ2+θ4−θ3≤β4+γ23，这种验证是即时的，因为我们假设至少有以下之一M. Magnin等人理论计算机科学电子笔记144（2006）5971不等式满足：β2+γ41<β4+γ21α4−γ12<α2−γ14β2+γ43<β4+γ23α4−γ32<α2−γ34因此，在结果域中，出现了非DBM多面体形式这与其它约束无关。因此，DBM过度近似放松了这一约束。我们还得证明这个倒数。 为了做到这一点，让我们试着证明这个矛盾。然后，假设父类不包括活动转换和挂起转换两者，使得这两个转换在触发tf之后保持启用（然后立即的是过度近似域等于精确域）或者没有验证了αk−γijetβk+γji上的两个不等式（第二种情况意味着可能产生的多面体约束与在θi和θj上分别获得的约束，这意味着我们在这里没有非DBM约束）。然后，DBM-over-approximation不放松任何约束。然后证明了声称的结果 Q4一种改进的离散TPN实际上，在研究调度-TPN时，我们观察到DBM-过逼近经常放松约束。这意味着，在许多情况下，当我们想要对系统进行更精确的验证时，可能需要精确的计算。操作一般多面体的主要缺点是在计算速度和内存使用方面的性能损失。该算法的主要思想是，当多面体可以存储为DBM时，我们并不总是需要操纵这些多面体。每次我们可以使用DBM，我们使用它们而不是一般的多面体。此外，我们使用定理3.2来先验地确定DBM计算何时放松约束。如果充要条件成立，那么我们就可以肯定多面体计算是必要的。否则，我们使用DBM操作，这要快得多因此，我们的算法混合了DBM操作和多面体操作，在必须操作的数据结构的功能我们的方法的优点可以很容易地理解一个简单的例子。让我们看看图5的网。节点和转换M. Magnin等人理论计算机科学电子笔记144（2006）5972P1，γ= 1，ω= 1t1[4， 5]图五. 只有一个状态类不能用DBM{P1，P2，P4}C08>4≤θ1≤50≤θ2≤ 3>：2≤θ4≤ 4t2t48>1≤θ1≤ 5>8>θ≤3t1>1≤θ3≤2<>1个{P1，P3，P4}C1>0≤θ≤4{P1，P2}C20≤θ2≤1>>4：0≤θ1−θ4≤3：1≤θ1−θ2t4t2t3t1{P1，P4}C38>θ1≤50≤θ4≤ 3>：1≤θ1−θ4{P1，P3}C48>1≤θ10≤θ3≤ 2>：θ1+θ3≤5{P1，P3}C58<1≤θ1≤ 3：1≤θ3≤ 2t4t3t3{P1}C6n1≤θ1≤ 5{P1}C7n1≤θ1≤ 3图六、图5的调度-TPN的状态类图·P2·P4·t2[0，3]t4[2，4]P3，γ= 1，ω=2t3[1，2]>M. Magnin等人理论计算机科学电子笔记144（2006）5973M如果（当前域D由DBM编码并且不满足条件3.2），则进行[14]的DBM计算，给出DJ其他进行多面体计算，给出DJend If如果（DJ可以由DBM编码），则通过DBM对DJend Ifreturn（MJ，DJ）对于精确计算和过度近似计算（8个节点和10个转换）是相同的这并不意味着通过DBM过近似和通过多面体算法获得的状态类图是相同的。这里的差别只存在于一个类中。通过执行触发序列t2.t4，得到的类C4如下：⎧{P1，P3}，、θ0≤θ1≤ 1， 0≤θ3≤ 2，θ1 +θ3≤ 5DBM-over-approximation导致类似的类，除了最后一个不等式不出现在相关的域中。即使考虑或不考虑这个不等式，从这个类只有一个可触发的转换：t3。在触发t3之后，DBM-over-approximation和精确计算导致相同的类C6：⎧{P1}，、θ1≤θ1≤ 5，对于下一个类（将通过触发t1获得），不需要操作一般多面体（除非定理3.2的条件得到验证）：DBM是足够的。因此，我们将结果域存储为DBM，并对该数据结构进行操作。我们方法的核心依赖于计算类的后继的算法算法1：用于计算下一个类的混合方法（入口参数：当前类C=（M，D）和触发的转换tf;结果：下一个类CJ=（MJ，DJ））M. Magnin等人理论计算机科学电子笔记144（2006）5974从类C=（M，D）计算可触发转换列表的方法对于DBM形式的类和更一般的多面体形式的类是相同的。检查活动转换ti是否可固定如下执行：对于所有活动转换tj，j/=i，我们将约束θi≤θj添加到当前域D，然后检查结果域是否为空。如果不是，这意味着转换ti可以从类C=（M，D）开始。唯一的区别是我们操作的域的性质：DBM或更一般的多面体。第二节介绍了经典的状态类图方法，Lime等人提出的DBM-过近似。改进算法已在IRCC y N开发的时间Petri网分析工具ROMEO[9]中实现。虽然DBM操作使用自制库，但多面体操作是通过多面体库New Polka完成的[12]。在下一部分中，我们比较了三种方法给出的结果我们的混合方法的结果，由于一般的多面体计算和DBM过近似。5实验结果为了说明我们的工作的优点，我们引入了一个基准，比较的效率，在计算速度方面，由L ime等人提出的DBM过近似。 在[14]中，经典的多面体计算和我们的混合算法。所有这三种方法实际上都已在ROMEO[9]中实现，R omeo是IRCCY N开发的时间Petri网分析工具。我们已经执行了不同的算法的例子来自实时系统。主要结果总结在表1中：我们给出了所得到的状态类图的节点和转换的数量以及在POWERPCG4，1.33 GHz，1GB RAM上的计算持续时间NA（不可用）意味着计算无法在所使用的机器上产生结果。对于DBM-over-approximation，NA意味着过近似状态空间导致无限数量的标记，而调度-TPN是有界的。可以肯定的是，当只有少数几个类可以转化为DBM时，我们的混合方法效率较低，并且可能比原始多面体方法慢一点（因为要检查生成的多面体是否可以像DBM一样编写）。但是对于更大的系统，我们在使用我们的混合方法计算精确的状态类图时观察到了显著的时间增益。这通过实施例4、5或6说明。此外，全多面体计算有时会导致内存超过内存，而我们的M. Magnin等人理论计算机科学电子笔记144（2006）5975生物素-TPN过度逼近精确计算多面体算法混合算法时间节点过渡时间节点过渡时间节点过渡实施例10.03 s21310.23秒18250.23秒1825实施例20.03 s540.19秒540.19秒54实施例385.52秒1517849135NANANA85.59秒1517849135实施例46.63秒22605700三十三点五十一秒226057006.69秒22605700实施例5十八点八八秒111672585680.9秒111672585619.08秒1116725856实施例66.45秒22255371二十三点五十一秒222553716.61秒22255371实施例70.03 s8100.18秒8100.18秒810实施例8九十九点六六秒1632354688NANANA九十九点七三秒1632354688实施例9NANANA0.19秒19240.19秒1924实施例10NANANA26.92秒45288699十三点二十四秒45288699实施例11NANANANANANA115.11秒1665032865实施例121.724781137NANANANANANA表1DBM-over-approximation算法、经典多面体算法和我们的混合算法之间的比较（POWERPCG4;1.33 GHz; 1GB RAM）混合方法执行计算而没有任何困难（示例3和11）。第一个结论是，对于所有实际感兴趣的系统，我们的混合方法在计算调度TPN的精确状态空间方面比一般的全多面体方法有效得多一般来说，DBM近似比精确计算快，这并不奇怪当由DBM过近似增加的状态数变得重要时，情况不再如此。这种极端情况出现在例子9、10和11中：由DBM-over- approximation添加的状态导致无限多个标记，而调度TPN是有界的。然而，有界调度-TPN上的精确状态空间计算不一定会终止（因为可访问性问题是不可判定的[3]），在这种情况下，DBM过度近似可以使获得状态空间的有限（但近似）抽象成为可能，如例12所示6结论在本文中，我们研究了一个标准，使我们能够知道一个先验的非DBM多面体形式将出现在域中的状态类的TPN秒表，当计算一个状态类的继任者。我们证明了一个必要和充分的条件，以确定是否DBM过近似放松的限制相比，精确的计算。M. Magnin等人理论计算机科学电子笔记144（2006）5976从这个条件出发，我们提出了一个计算调度TPN的精确状态类图的有效算法。测试表明，我们的算法是所有系统的实际利益更好（在执行时间和内存方面）比经典的方法在计算精确的状态空间。特别地，它允许我们计算一些调度TPN的状态类图，对于这些调度TPN，全多面体算法的存储器消耗太高，并且对于这些调度TPN，DBM过度近似引入了无限数量的标记（并且无论如何只计算近似值状态空间）。值得注意的是，虽然它允许我们自己检查时间特性（例如通过使用观察者），但它也可以作为[5]和[15]方法中DBM过度近似的（较慢但仍然有效）替代品，当DBM过度近似引入无限数量的标记时，而网络实际上是有界的，并阻止这些方法产生结果。现在，也可以对过近似方法进行改进。提出的DBM-over-approximation李梅等人[14]显然未来的工作还包括研究离散语义，它提供欠近似，但将验证问题转置到有限状态空间。引用[1] Avis，D.，K. Fukuda和S.Picozzi，关于凸多面体的正则表示，在：A。M.科恩，X.- S. Gao和N.Takayama ， editors ， Mathematical Software ， Proceedings of the First InternationalCongress of Mathematical Software（2002），pp. 350-360[2] 贝托米厄湾和M.Diaz，Modeling and Verification of Time Dependent Systems Using TimePetri Nets，IEEE Transactions on Software Engineering17（1991），pp.259-273。[3] Berthomieu，B. ，D. Lime ，O. Roux和F. Vernadat，Reachability problems and abstractstate spaces for time Petri nets with stopwatches，Technical Report 04483，Applanatoired'Analyse et d'Ar chi t e cture de es Syst ` eme s（L AA S），T ou l ou se，Fran n c e（2004）.[4] 贝托米厄湾和M. Menasche，An Enumerative Approach for Analysis Time Petri Nets. ，IFIPCongress Series9（1983），pp. 41比46[5] Bucci，G.，A. 费代利湖Sassoli和E.Vicario，实时抢占式系统的时间状态空间分析，IEEE软件工程学报30（2004），pp.97-111[6] Cassez，F.和K.拉森，秒表的惊人力量，在：C。Palamidesi，编辑，第11届并发理论国际会议（CONCUR138-152[7] Dantzig，G.，Linear programming and extensions，IEICE Transactions on Information andSystems（1963）.[8] Dill，D.，有限状态并发系统的时序假设和验证，407，1989，pp。197-212M. Magnin等人理论计算机科学电子笔记144（2006）5977[9] Gardey，G.，D. Lime，M.Magnin和O.H. Roux，Romeo：A tool for analyzing time petrinets ， in ： Proceedings of he 17th International Conference on Computer-AidedVerification（CAV）（2005）.[10] Henzinger，T.，P. - H. Ho和H.Wong-Toi，Hytech：混合系统的模型检查器，Journal ofSoftware Tools for Technology Transfer1（1997），pp.110-122[11] Henzinger，T.，P. Kopke，A. Puri和P.Varaiya，关于混合自动机的可判定性是什么？Journal ofComputer and System Sciences57（1998），pp.94-124.[12] Jeannet，B.，凸多面体库，发布1.1.3c版，可在http://www.irisa.fr/prive/Bertrand.Jeannet/newpolka.html（2002年）的报告。[13] Larsen，K.，Pettersson和W. Yi，实时系统的模型检测，在：计算理论基础，1995年，pp. 62比88[14] Lime，D.和O.鲁，扩展时间Petri网调度的表达性和分析，第五届IFAC现场总线系统及其应用国际会议，（FET 2003）（2003）。[15] Lime，D.和O.Roux，一种基于调度的扩展时间Petri网的时间分析方法，在：第25届IEEE实时系统研讨会（RTSS 2004）（2004），pp. 187- 196.[16] Roux，O.和A.-M.D'eplannche，Extennsiondesr'eseauxdePetrit-temporelspourlamod'elisationdel'or donnan c e m en t d e t tachache ste m ps- r' ee l，in：3 e cong r `es M o d 'el327-342[17] 鲁岛和D. Lime，Time Petri nets with inhibitor hyperarcs.形式语义和状态空间计算，在：第25 届国 际 会 议 上的 应 用 和 理 论 的Petri 网 ， （ ICATPN 2004 ） ， 讲 义 在 计 算 机 科 学 3099（2004），页。371-390.[18] Ro u x，O. H. 和A. -M. 陈文辉，一种基于多变量系统建模方法的计算机仿真系统，北京大学出版社，2002年。
我的内容管理
收起
我的收益 登录查看自己的收益
我的积分
登录查看自己的积分
我的C币
登录后查看C币余额
我的收藏 
我的下载 
下载帮助 
