logo

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

More info
  • ReceivedNov 20, 2017
  • AcceptedMay 7, 2018
  • PublishedNov 1, 2018

Abstract

There is no abstract available for this article.


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

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

京ICP备18024590号-1