SCIENCE CHINA Information Sciences, Volume 61, Issue 12: 129104(2018) https://doi.org/10.1007/s11432-017-9446-3

## New reachability trees for analyzing unbounded Petri nets with semilinear reachability sets

• AcceptedMay 7, 2018
• PublishedNov 1, 2018
Share
Rating

### Supplement

Appendixes A and B.

### References

[1] Karp R M, Miller R E. Parallel program schemata. J Comput Syst Sci, 1969, 3: 147-195 CrossRef Google Scholar

[2] Wang F Y, Gao Y, Zhou M C. A modified reachability tree approach to analysis of unbounded Petri nets. IEEE Trans Syst Man Cybern B, 2004, 34: 303-308 CrossRef Google Scholar

[3] Ru Y, Wu W M, Hadjicostis C. Comments on “a modified reachability tree approach to analysis of unbounded Petri nets". IEEE Trans Syst Man Cybern B, 2006, 36: 1210-1210 CrossRef Google Scholar

[4] Wang S G, Zhou M C, Li Z W. A new modified reachability tree approach and its applications to unbounded Petri nets. IEEE Trans Syst Man Cybern Syst, 2013, 43: 932-940 CrossRef Google Scholar

[5] Wang S G, Gan M D, Zhou M C. Macro liveness graph and liveness of $\omega$-independent unbounded nets. Sci China Inf Sci, 2015, 58: 032201 CrossRef Google Scholar

[6] Ginsburg S, Spanier E. Semigroups, Presburger formulas, and languages. Pac J Math, 1966, 16: 285-296 CrossRef Google Scholar

[7] Hauschildt D. Semilinearity of the reachability set is decidable for Petri nets. Dissertation for Ph.D. Degree. Hamburg: University of Hamburg, 1990. Google Scholar

[8] Lambert J L. Vector addition systems and semi-linearity. SIAM J Comput, 1994. Google Scholar

[9] Yen H C. Path decomposition and semilinearity of petri nets. Int J Found Comput Sci, 2009, 20: 581-596 CrossRef Google Scholar

•

Algorithm 1 Construction of an NRT

Require:An unbounded net $(N,~\mu_0)$;

Output:An NRT of $(N,~\mu_0)$;

Let $x_0$ be the root node of the tree and $\mu_0$ the marking of node $x_0$;

$\Xi:=\{x_0\}$ and label $x_0$ as a new node;

while there exists a new node $x$ in $\Xi$ do

Label $x$ as an old node and let $\mu_x$ be the marking of node $x$;

for each $t\in~T$

if $t$ is enabled or conditionally enabled at $\mu_x$ then

Compute the next-state $\delta(\mu_x,~t)$ and create a new node $z$ in the NRT;

if there exists a node $y$ on the path from the root node to $x$ such that $\delta(\mu_x,~t)>\mu_y$ and $\delta(\mu_x,~t)~\nsubseteq~\mu_y$ then

if $\delta(\mu_x,~t)$ is an ordinary marking then

$j=1$;

else

$j=1+g$, where $g$ is the maximal dimension of all the $\omega$-numbers in $\delta(\mu_x,~t)$;

end if

for each $p\in~P$

if $\delta(\mu_x,~t)(p)>~\mu_y(p)$ then

$\mu_z(p):=\delta(\mu_x,~t)(p)+k\omega^{(j)}$, where $k=\delta(\mu_x,~t)(p)-\mu_y(p)$;

else

$\mu_z(p):=\delta(\mu_x,~t)(p)$;

end if

end for

else

$\mu_z:=\delta(\mu_x,~t)$;

end if

end if

if $t$ is enabled at $\mu_x$ then

Add a solid arc $t$ from $x$ to $z$; /$\ast$ $t$ is enabled at $\mu_x$ $\ast$/

else

Add a dotted arc $t$ from $x$ to $z$; /$\ast$ $t$ is conditionally enabled at $\mu_x$ $\ast$/

end if

if $z$ is a terminal node, $\omega$-duplicate node, or duplicate node then

Let node $z$ be an old node;

else

Let node $z$ be a new node;

end if

$\Xi:=\Xi\cup\{z\}$;

end for

end while

Citations

• #### 0

Altmetric

Copyright 2020 Science China Press Co., Ltd. 《中国科学》杂志社有限责任公司 版权所有