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

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

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

Legal firing transition sequence （LFS for short） of Petri Net is a sub-problem of reachability. The previous LFS decision algorithm fails in EXE-time complexity and could not be adopted in general Petri net. To overcome these disadvantages, an algorithm integrating linear algebra and reachable tree was proposed. Since a T-invariant indicated a LFS marked on loop in reachable graph, the solution vector of state equation could be separated into two parts ： linear combination of minimal T-invariant and a basic vec- tor which did not contain any minimal T-invariant. So, the original LFS decision was reduced to that of basic vector. Reachable trees of both original petri nets with initial marking and inversed petri net with target marking were constructed in layer order by turns. Simultaneously, markings in current leaf layer of reachable trees were compared to find an equal marking. Analysis shows that the time complexity of this algorithm is polynomial, which is applicable to other similar algorithms.