一种有界Petri网的可诊断性验证方法

Diagnosability verification of bounded Petri nets

离散事件系统满足可诊断性是设计故障诊断算法的前提,因此研究可诊断性验证方法具有重要意义.故障发生后无死锁是研究可诊断性问题常见的假设之一,限制了可诊断性验证方法的应用范围.本文在去掉故障发生后无死锁假设的基础上,首先提出了标签可达图的概念和构建算法,其次提出了一种新的可诊断性验证算法来验证有界Petri网是否满足可诊断性.最后通过例子详细说明可诊断性验证算法的计算过程.

It is important to study diagnosability verification method because it is the premise of designing fault diagnosis algorithm for discrete event system to satisfy the diagnosability.Deadlock-free after a fault is one of the common assumptions in the research field of diagnosability,which limits the application scope of diagnosability verification method.In this paper,we remove the assumption of deadlock-free after the occurrence of a fault.The concept and construction algorithm of the label reachability graph are proposed first.Then a new diagnosability verification algorithm is given to verify diagnosability of bounded Petri nets.Finally,an example is given to illustrate the calculation process of the algorithm.