一种基于进程验证的Petri网可达性判定方法

A Reachability Determining Algorithm of Petri Net Based on Process Verification

为了解决Petri网的可达性判定问题,提出了一种基于进程验证的可达性判定方法.通过分析Petri网基本进程段子段间偏序关系,该方法提出原子进程段概念,求得原子进程段集及其偏序关系集作为可达性判定的验证对象.基于原网状态方程解向量、原子进程段T-向量的线性纯整数规划问题解,选取该解中非零分量对应的原子进程段子集作为待验进程段集,选取待验进程段间的偏序关系子集作为待验推理规则集,通过验证是否存在这两个集合上的以初始标识M0为推导初态、目的标识Md为推导终态的序列而判定(M0,Md)是否可达.分析表明该可达性判定算法的时间复杂度是依赖于原子进程段集规模的,最坏情况下不超过变迁集规模.

In this paper, a process verification based algorithm is proposed to solve the reachability determining problem of Petri net. At first, the definition of atomic process section is introduced based on the partial relation decomposition, and the atomic process section set and the par- tial relation set are sought to act as verified objects in reachability determining. After the solution vector to pure linear nonequivalent expression of state equation solution vector and T-vectors of atomic process sections is calculated, a subset is selected from the atomic process section set with the standard that each element of the subset corresponds to a nonzero component in the solution vector. The partial relation is picked out to form the partial relation subset if it just describes par- tial relation between two elements of the atomic process section subset. If there is a reductive se- quence which explores source marking as start state and target marking as end state, the reachability of Petri net could be concluded. The analysis shows that the time complexity of this determining algorithm depends on the scale of atomic process section set, and is no more than the scale of transition set under the worst condition.