中文

Journal of Applied Sciences >

2020 , Vol. 38 >Issue 5: 695 - 712

DOI: https://doi.org/10.3969/j.issn.0255-8297.2020.05.004

Novel Technologies for Intelligent Computing

Place Bound Algorithm of Petri Net Based on Partial State Space Storage

Expand
  • 1. College of Electricity and Information Engineering, Tongji University, Shanghai 201804, China;
    2. Key Laboratory of the Ministry of Education for Embedded System and Service Computing, Tongji University, Shanghai 201804, China;
    3. Shanghai Electronic Transactions and Information Service Collaborative Innovation Center, Tongji University, Shanghai 201804, China

Received date: 2020-05-25

  Online published: 2020-10-14

Fold

Abstract

Petri net is an important formal modeling tool, and boundedness is one of the important properties of Petri net. In this paper, we focus on this property and propose a new algorithm to solve the place bounds of Petri net without storing all state spaces. The main idea is that in the process of generating state spaces, we can accurately solve the bounds of all places by storing partial states through eliminating some loops of reachability graph and taking advantages of related properties of T-invariant. Experimentally, we compare several other methods with the proposed one in their capability of solving place bounds with the open data set of model checking contest, and results show the effectiveness of the proposed algorithm.

Key words： Petri net; boundedness; state space; bit storage

Cite this article

LU Weihong, DING Zhijun . Place Bound Algorithm of Petri Net Based on Partial State Space Storage[J]. Journal of Applied Sciences, 2020 , 38(5) : 695 -712 . DOI: 10.3969/j.issn.0255-8297.2020.05.004

References

[1] Petri C A, Reisig W. Petri net[J]. Scholarpedia, 2008, 3(4):6477.
[2] Colom J M, Silva M. Improving the linearly based characterization of P/T nets[C]//International Conference on Application and Theory of Petri Nets. Springer, Berlin, Heidelberg, 1989:113-145.
[3] Finkel A. A minimal coverability graph for Petri nets[J]. Application and Theory of Petri Nets, 1991:1-21.
[4] Wolf K. How Petri net theory serves Petri net model checking:a survey[C]//Transactions on Petri Nets and Other Models of Concurrency XIV, Springer, Berlin, Heidelberg, 2019:36-63.
[5] Schmidt K. Using Petri net invariants in state space construction[C]//International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer, Berlin, Heidelberg, 2003:473-488.
[6] Schmidt K. Lola:a low level analyser[J]. Application and Theory of Petri Nets, 1999, 1825:465-474.
[7] 吴哲辉. Petri网导论[M]. 北京:机械工业出版社, 2006.
[8] Clarke E M, Grumberg O, Peled D. Model checking[M]. Cambridge:MIT Press, 1999.
[9] Amparore E, Berthomieu B, Ciardo G. Presentation of the 9th edition of the model checking contest[C]//International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer, Cham, 2019:50-68.
[10] Heiner M, Donaldson R, Gilbert D. Petri nets for systems biology[J]. Symbolic Systems Biology:Theory and Methods, 2011:61-97.
Options
Outlines

/

〈 〉