基于T-不变量消除的Petri网合法变迁引发序列判定算法

Petri网的合法变迁引发序列问题(LFS)是其可达性问题的子问题.前人在LFS判定时常因判定算法的指数级时空复杂度或算法难以推广至一般Petri网而受限.因此,基于Petri网T-不变量支集变迁与可达图有向环路上标注变迁的对应关系,综合应用线性代数与可达树分析,原LFS判定被缩减为以基础向量为发生数向量的LFSb判定.通过两棵可达树(分别以原网、初始标识;逆网、目的标识为根)层序轮流构造同时比较当前叶节点层中的标识,若算法终止前有相同标识出现,则LFSb(LFS)判定成功;反之,LFS判定失败.分析表明,算法的时间复杂度为多项式级别的,且适用于一般Petri网的LFS判定.

Decision algorithm for legal firing transition sequence of Petri net based on T-invariant eliminating

Legal f iring t ransit ion sequence ( LFS for short ) of Pet ri Net is a sub-problem of reachability . The previous LFS decisio n algor ithm fails in EXE-t ime complexity and co uld not be ado pted in g eneral Pet ri net . T o ov ercome these disadv antages, an algo rithm integ rat ing linear algebr a and r eachable tree w as pr opo sed. Since a T -invariant indicated a LFS marked on loop in reachable gr aph, the so lut ion vector of state equat ion could be separated into tw o part s: linear combinat io n of minimal T -invariant and a basic vecto r w hich did no t contain any minimal T -invariant . So , the original LFS decision w as reduced to that of basic vecto r. Reachable tr ees o f both original pet ri net s with init ial marking and inversed petr i net w ith target marking w er e const ructed in layer o rder by turns. Simultaneously, markings in current leaf layer of reachable tr ees w er e compared to find an equal marking . Analysis show s that the t ime complex ity of this algo rithm is polynomial, which is applicable to other similar algo rithms.