Petri网顺序序列的测试与判定.doc

第七章 Petri网顺序序列的测试与判定7.1 引言Petri网合法发射序列的判定问题是网论中一重要研究课题，它是许多网论问题的直接基础，如：时延Petri网的经典的调度问题 1-3 和循环调度问题 12, 14, 16都能被归结为这类判定问题；Petri网极小初始标识的配置问题 8-10,13,15 也能被转化为这类判定问题；还有众所周知的Petri网可达性问题 4-6 更是以这类判定问题为基础。在 8, 9, 11 中，Petri网合法发射序列的判定问题被深入研究，多项式判定算法被给出，时间复杂性被分析。研究获知，这类判定问题对于一般Petri网，甚至对于某些自由选择网都是NP-完全问题 11。而仅仅对于几个简单网类，如：坚持网、无冲突网和状态机网，这类判定问题才是多项式可解的。文 16 考虑了Petri网合法发射序列的判定问题的一个近似问题，从而给出近似问题的一个多项时间算法。由此足见，Petri网合法发射序列的判定问题一般而言是一类困难问题。另一方面，这类问题又是网论中的十分重要而基础的问题。因此，这项工作的每一点推进都是非常重要的。文21研究了坚持网、无冲突网和状态机网的同步合成网类，获得了这一网类合法发射序列判定问题的多项式判定算法，从而对以往的工作有了重要推进。在这一章中，我们将着重介绍Petri网的合法发射序列的判定问题和合成过程中序列测试等问题的有关算法。7.2 发射序列测试为了验证系统的功能，测试系统功能的保持性，就是要测试系统的发射序列是否被保持到目标系统。复杂系统的发射序列的测试是一个困难问题，分解复杂系统和分布测试集成求解的方法是解决此问题的一种有效途径。下面具体来讨论这种方法。定理 7.1 设是两个Petri网, , 且 。若 ，则 当且仅当 。证明 因为 ，则 当且仅当 : ； 当且仅当 ； 当且仅当 。从定理3.4，我们有。定理 7.2 设是两个Petri网, , 且。则 当且仅当 。证明 根据引理6.1、定理7.1，易证本结论是正确的。基于定理7.1和定理7.2 , 我们可以得到下面的测试算法。 算法 7.1 Shufting_Test输入 输出 / 若 则，否则 。/(1) begin(2) for to do(3) if then(4) (5) else (6) endif(7) endfor(8) endbegin.算法 7.2 Beloning_Test输入 输出 / 若 则 ，否则 。/(1) begin(2) 基于可达图生成算法，产生的可达图; (3) for to do(4) if then(5) (6) else (7) endif(8) endfor(9) endbegin.显然，算法 Shufting_Test 只需要一些投影操作和比较操作，而算法 Beloning_Test 只需要一些投影操作和测试子系统的发射序列。因此，测试过程的复杂性被化简。例 7.1 在图6.1的Petri网中，有一组 序列 。现在要测试是否为真，这里。利用先前描述的算法Shufting_Test，测试结果如下面的两个表 (当 )。 表7.1：对于10个序列的算法Shufting_Test的测试结果 =? ? acdeba gabfa aba aba = bebeac bfab bba bab no acdebe bfaga ab baa no beacde bfag ba ba = beacde bfaga ba baa no acdeb gabf ab ab = acdeb gabfag ab aba no beacde bfag baa ba no beac bfag ba ba = bebea bfabf bba bab no 例 7.2 图6.1中的Petri网有一组序列，现在要测试。 利用前面描述的算法Beloning_Test，其测试结果如下面的表7.2中显示 ( 这里 ) 。表7.2: 对于10个序列的算法Beloning_Test 的测试结果 ? ? ? abefabef abeabe abfabf befacdea beacdea bfaa gacgdeacde acdeacde gaga gacbed acbed gab bfdecabc bdecabc bfab bfeacdea beacdea bfaa fgcdeac cdeac fga befagcdeac beacdeac bfaga gacgde acde gag gacdega acdea gaga 7.3 合法发射序列的判定Petri网合法发射序列的判定问题可以被形式化地描述如下：给定一个Petri网和一个非负整数的维向量，现在要判定是否存在的一个合法发射序列（即：），使得是的发射向量（即：，都有）。7.3.1. 算法基础首先，我们引进一些必要的概念，然后对同步合成网的一些语言性质进行研究，这将为后面的算法提供基础。引理 7.1 设 是一个字母表，且。, 令。则，这里。证明 当且仅当 当且仅当 。 引理 7.3 设是两个Petri网，且。若，则 当且仅当 。证明 当且仅当 ( 据引理6.1 ) 当且仅当 , 当且仅当 : , 当且仅当 。 ( 根据引理7.1 ) 定义7.1 设是两个字母表，且。分别是上的一个语言，对于，令 ，则称是的同步序列集。若是对应于的发射向量, ，且，令，使得：(1) 若，则；(2) 若，则。则称是的同步发射向量。定义7.2 设是个Petri网，是的发射序列，是对应于的发射向量, 。则记：；。引理7.3 设是两个Petri网，。是的维非负整数向量，。则是的发射向量当且仅当(1) 是的发射向量；(2) ，其中是对应于的一个发射序列。证明 () 由于是的发射向量，则存在一个对应于的发射序列。令，又由于，即，则是对应于的一个发射序列。因此，是的发射向量。从而 (1) 成立！同时，根据引理7.1可知 (2) 也成立！() 由于是的发射向量，则存在一个对应于的发射序列。又由于，则根据引理7.3可知，从而，使得。又由于是的对应于的发射序列，同时，即。因此是的对应于的发射序列，从而是的发射向量。综上所述，故结论得证！ 定理7.3 设是个Petri网,是的维非负整数向量，。则是的发射向量当且仅当(1) 是的发射向量；(2) ，其中是对应于的一个发射序列, 是对应于的一个发射序列, 。证明 由于操作 和 均满足结合律，因此我们按照下面图7.1的思路两两结合地应用引理7.3即可证明该结论成立！存在对应与的发射序列存在对应与的发射序列存在对应与的发射序列不是发射向量是发射向量存在对应与的发射序列 yes yes no no yes no no yes no no yes no yes yes图7.1 定理7. 1的证明思路定理7.4 设是个Petri网,。则.证明 ，其中，则，使得。令，则有 从而。另一方面，反证。若，但是。这样，都有。而，令。则 这与假设矛盾！因此，。综上所述，结论成立！ 7.3.3 判定算法基于定理7.3和定理7.4，一个同步网的合法发射序列的判定算法被描述如下。算法7.3 (合法发射序列的直接分解测试）输入 , 输出 / 若：使得 则 , 否则 。/(1) begin(2) for to do(3) ;(4) 对于和调用文11中的算法进行求解; / 若: 使得 则 , 否则 /(5) if then ;(6) goto (24);(7) endif;(8) endfor;(9) ; ;(10) for to do(11) ;(12) ；(13) ;(14) ;(15) ;(16) for to do(17) ;(18) ;(19) endfor;(20) if then ;(21) goto (24);(22) endif;(23) endfor;(24) endbegin.7.3.4 算法复杂性在这一节里，我们将对上述判定算法的时间复杂性进行分析。其中，将用到文献8,9,11中的一些结论。在文献8,9,11中已经证明：（I）Petri 网的合法发射序列测试问题是 NP-完全问题 。（II）对于一个坚持Petri网，判定一个非负整数的维向量是否为的一个发射向量的时间复杂性是。由于无冲突Petri网也是坚持Petri网。因此，无冲突Petri网的判定时间复杂性也不超过。（III）对于一个状态机Petri网，判定一个非负整数的维向量是否为的一个发射向量的时间复杂性是。定理7.5 设是个Petri网，它们或者坚持Petri网、或者是无冲突Petri网、或者是状态机Petri网。，是一个非负整数的维向量。则判定是否为的一个发射向量的时间复杂性是。证明 算法中计算的计算量是，根据上面的已知结论(II)和(III)可知，对于和调用文11中的算法进行求解的计算量是，而判定的计算量是1。这样一来，算法中(2)-(8)的计算量是。算法中计算的计算量是，计算的计算量也是，计算的计算量是，(14)-(17)的计算量是，计算的计算量是，而判定的计算量是。这样一来，算法中(2)-(8)的计算量是,因此，本算法的计算量是+。7.3.5 例子图6.1中显示的是两个状态机Petri网和它们的同步合成网。若我们知道非负整数向量 现要判定是否为Petri网的发射向量 ? 容易看出Petri网非坚持网、非无冲突网和非状态机网。因此，不能直接应用文8, 9, 11中的判定算法进行判定。但是，网是两个状态机Petri网的同步合成网。这样一来，可以利用前面的基于同步合成（或者说同步分解）的判定算法进行判定。分析过程如下： 这样，。从而，因此，说明是Petri网的发射向量。定理 7.6 设是两个Petri网，, 且 ，则当且仅当 这里, 。利用定理7.1-7.5容易证明该结论为真。 例7.1 已知两个Petri 网, 它们的可达图, 它们的同步合成网 如图 7.2所示，现有以下三个问题：问题 1. 若,问 ?问题2. 若，问 ?问题3. 若，问 ? 图7. 2 两个 Petri 网的同步合成对于问题1. 由于 , 根据定理7.3我们有。对于问题2. 由于 根据定理7.4我们有.对于问题3. 由于。若取 , 则，根据定理7.5我们有。7.4 测试算法及其复杂性基于定理7.3-7.4及7.6，发射序列合法性和状态可达性问题的有关部门测试算法被分别描述如下：(1) 对于问题1 ，若, ，如何测试? 算法 7.4 (发射序列的合法shuffling运算测试)输入 输出 / 若 , 则 , 否则 . /(1) begin(2) ; ;(3) for to do(4) ;(5) ;(6) ;(7) ;(8) ;(9) for to do(10) ;(11) ;(12) endfor;(13) if then ;(14) goto (17);(15) endif;(16) endfor;(17) endbegin.(2) 对于问题2 ，如何测试? 下面介绍相关测试算法，这里算法7.5被用于规模较小的Petri网的合法发射序列的测试问题，而算法7.6被用于规模较大的Petri网的合法发射序列的测试问题。算法 7.5 (合法发射序列的直接测试)输入 / 记 /输出 / 若 , 则 , 否则 . /(1) begin(2) ;(3) for to do(4) for to do(5) if then(6) (7) else ; goto (11)(8) endif(9) endfor(10) endfor(11) endbegin.算法 7.6 (合法发射序列的分解测试)输入 , 输出 / 若 , 则 , 否则 . /(1) begin(2) for to do(3) ;(8) if PCSPN , then 调用文献8, 9, 11中的算法; / 若 , 则 ; 否则 . 这里 PCSPN 表示坚持网、自由选择网和状态机Petri网的集合/(9) else 调用算法7.5; / 若 , 则 ; 否则 . /(10) endif(11) if then ;(12) goto (12);(13) endif(14) endfor(15) ;(12) endbegin.(3) 对于问题3，如何测试? 则有如下算法：算法 7.7 (可达性分析)输入 , 及它们的同步合成网 输出 / if then , otherwise /(1) begin(2) 求线性方程组的最小解;(3) for to do(4) ;(5) if PCSPN , 调用文献8, 9, 11中的算法; / 若 : 使得 , 则 ; 否则 /(6) else 直接求解 ; / 若 :使得, , then ; otherwise /(7) endelse(8) if then ;(9) goto (13);(10) endif;(11) endfor;(12) For , 调用算法7.4; / 若 ,则 , 否则 . /(13) endbegin.显然，算法7.4只需做较少的投影和比较操作，而算法7.6只需做较少的投影操作和子系统的测试。因此测试大系统的复杂性已经被化简，算法7.7也是如此，下面将讨论算法的复杂性。定理7.6. Petri网的合法发射序列的测试问题是NP-完全问题。定理7.7. 设PCSPN是坚持网、自由选择网和状态机Petri网的集合，Petri网 PCSPN，则的合法发射序列的测试问题的复杂性是 。定理7.8 算法7.4的复杂性是。证明. 在算法7.4中，计算的时间复杂性是，计算的时间复杂性是，计算的时间复杂性是。步骤 (7)-(10) 的时间复杂性是，计算的时间复杂性是，测试的时间复杂性是。因此，算法7.4的时间复杂性是。定理7.9 算法7.5的时间复杂性是。证明. 结论是显然的。定理7.10 算法7.6的时间复杂性是。证明 根据定理7.7和定理7.9，算法7.6的时间复杂性是。定理7.11 设个Petri网 PCSPN, ， 。则测试的时间复杂性是，这里是状态方程的极小解。证明. 在算法7.7中，求状态方程的极小解 的时间复杂性是；计算的时间复杂性是；对于和，计算的时间复杂性是；测试的时间复杂性是1；这样，步骤 (3)-(11) 的时间复杂性是。根据算法7.7，步骤 (12) 的时间复杂性是。因此，算法7.7的时间复杂性是。7.5 一个实际系统的分析图7.3是高速罐头包装机原型，下面通过它来说明同步逻辑设计方法。包装机包括六个相互独立的部分：轴、进料机、滚筒1、滚筒2、传送带和驱动器，它们的转换可以从进料机到滚筒1，滚筒1到滚