TY - JOUR

T1 - A reachability determining algorithm of Petri net based on process verification

AU - Yu, Feng

AU - Luo, Jun Zhou

AU - Li, Wei

AU - Wang, Peng

PY - 2010/2

Y1 - 2010/2

N2 - 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 partial 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 partial relation between two elements of the atomic process section subset. If there is a reductive sequence 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.

AB - 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 partial 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 partial relation between two elements of the atomic process section subset. If there is a reductive sequence 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.

KW - Petri net

KW - Process of Petri net

KW - Process verification

KW - Reachability determining

UR - http://www.scopus.com/inward/record.url?scp=77950564216&partnerID=8YFLogxK

U2 - 10.3724/SP.J.1016.2010.00288

DO - 10.3724/SP.J.1016.2010.00288

M3 - Article

AN - SCOPUS:77950564216

SN - 0254-4164

VL - 33

SP - 288

EP - 299

JO - Jisuanji Xuebao/Chinese Journal of Computers

JF - Jisuanji Xuebao/Chinese Journal of Computers

IS - 2

ER -