Modeling and reachability analysis of synchronizing transitions bounded Petri net systems based upon semi-tensor product of matrices

doi:10.1016/S1005-8885(17)60190-0

JOURNAL OF CHINA UNIVERSITIES OF POSTS AND TELECOM ›› 2017, Vol. 24 ›› Issue (1): 77-86.doi: 10.1016/S1005-8885(17)60190-0

Previous Articles Next Articles

Modeling and reachability analysis of synchronizing transitions bounded Petri net systems based upon semi-tensor product of matrices

Gao Na, Han Xiaoguang, Chen Zengqiang, Zhang Qing

1. College of Computer and Control Engineering, Nankai University
2. Tianjin Key Laboratory of Intelligent Robotics
3. College of Science, Civil Aviation University of China

Received:2016-08-19 Revised:2017-01-19 Online:2017-02-28 Published:2017-02-28
Contact: Chen Zeng-Qiang E-mail:chenzq@nankai.edu.cn
Supported by:
This work was supported by the National Natural Science Foundation of China (61573199, 61573200), the Tianjin Natural Science Foundation (14JCYBJC18700).

Abstract

Abstract: The reachability problem of synchronizing transitions bounded Petri net systems (BPNSs) is investigated in this paper by constructing a mathematical model for dynamics of BPNS. Using the semi-tensor product (STP) of matrices, the dynamics of BPNSs, which can be viewed as a combination of several small bounded subnets via synchronizing transitions, are described by an algebraic equation. When the algebraic form for its dynamics is established, we can present a necessary and sufficient condition for the reachability between any marking (or state) and initial marking. Also, we give a corresponding algorithm to calculate all of the transition paths between initial marking and any target marking. Finally, an example is shown to illustrate proposed results. The key advantage of our approach, in which the set of reachable markings of BPNSs can be expressed by the set of reachable markings of subnets such that the big reachability set of BPNSs do not need generate, is partly avoid the state explosion problem of Petri nets (PNs).

Key words: reachability, Petri nets, BPNSs, semi-tensor product (STP) of matrices, synchronizing transitions

Gao Na, Han Xiaoguang, Chen Zengqiang, Zhang Qing. Modeling and reachability analysis of synchronizing transitions bounded Petri net systems based upon semi-tensor product of matrices[J]. JOURNAL OF CHINA UNIVERSITIES OF POSTS AND TELECOM, 2017, 24(1): 77-86.

References

1. Ichikawa A, Hiraishi K. Analysis and control of discrete event systems represented by Petri nets. Discrete Event Systems: Models and Applications, 2006, 103(1): 115-134

2. Sarkar D, Das S K, Agrawal V K, et al. A new methodology for analyzing distributed systems modeled by Petri nets. International Journal of Computer Mathematics, 2007, 31(3): 153-165

3. Ma Z Y, Li Z W, Giua A. Design of optimal Petri net controllers for disjunctive generalized mutual exclusion constraints. IEEE Transactions on Automatic Control, 2013, 60(7): 1774-1785

4. Xiu J P, Xu Y T, Deng F, et al. A Petri net-based approach for data race detection in BPEL. Journal of China Universities of Posts and Telecommunications, 2010, 17(9): 10-15

5. Peleties P, Decarlo R. Analysis of a hybrid system using symbolic dynamics and Petri Nets. Automatica, 1994, 30(9): 1421-1427

6. Wu N Q, Bai L P, Chu C B. Hybrid Petri net modeling for refinery process. Proceedings of the 2004 IEEE International Conference on Systems, Man and Cybernetics (SMC’04): Vol 2, Oct 10-13, 2004, The Hague, Netherlands. Piscataway, NJ, USA: IEEE, 2004: 1734-1739

7. Murata T. Petri nets: properties, analysis and applications. Proceedings of the IEEE, 1989, 77(4): 541-580

8. Reisig W. Petri nets: an introduction. New York, NY, USA: Springer-Verlag, 1987

9. Bourdeaud’huy T, Hanafi S, Yim P. Mathematical programming approach to the Petri nets reachability problem. European Journal of Operational Research, 2007, 177(1): 176-197

10. Rathke J, Sobocinski P, Stephens O. Reachability problems. New York, NY, USA: Springer, 2014: 230-243

11. Reinhardt K. Reachability in Petri nets with inhibitor arcs. Electronic Notes in Theoretical Computer Science, 2008, 223: 239-264

12. Wimmel H, Wolf K. Applying CEGAR to the Petri net state equation. Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’11), Mar 26-Apr 3, 2011, Saarbrücken, Germany. LNCS 6605. Berlin, Germany: Springer, 2011: 224-238

13. Ramachandran P, Kamath M. A sufficient condition for reachability in a general Petri net. Discrete Event Dynamic Systems: Theory and Applications, 2004, 14(14): 251-266

14. Ahmad F, Huang H J, Wang X L. A technique for reachability graph generation for the Petri net models of parallel processes. International Journal of Electrical and Electronics Engineering, 2009, 3(1): 57-61

15. Chiola G, Dutheillet C, Franceschinis G, et al. A symbolic reachability graph for coloured Petri nets. Theoretical Computer Science, 1997, 176(1/2): 39-65

16. Notomi M, Murata T. Hierarchical reachability graph of bounded Petri nets for concurrent-software analysis. IEEE Transactions on Software Engineering, 1994, 20(5): 325-336

17. Pastor E, Cortadella J, Roig O. Symbolic analysis of bounded Petri nets. IEEE Transactions on Computers, 2001, 50(5): 432-448

18. Zhou K Q, Zain A M, Mo L P. A decomposition algorithm of fuzzy Petri net using an index function and incidence matrix. Expert Systems with Applications, 2015, 42(8): 3980-3990

19. Boucheneb H, Rakkay H. A more efficient time Petri net state space abstraction useful to model checking timed linear properties. Fundamenta Informaticae, 2008, 88(4): 469-495

20. Cheng D Z. Semi tensor product of matrices and its applications to Morgan’s problem. Science in China Series: Information Sciences, 2001, 44(3): 195-212

21. Qi H S, Cheng D Z. Analysis and control of Boolean networks: a semi-tensor product approach. Acta Automatica Sinica, 2011, 37(5): 1352-1356

22. Han X G, Chen Z Q, Zhang K Z, et al. Modeling and reachability analysis of a class of Petri nets via semi-tensor product of matrices. Proceedings of the 34th Chinese Control Conference, Jul 28-30, 2015, Hangzhou, China. Piscataway, NJ, USA: IEEE, 2015: 6586-6591

23. Han X G, Chen Z Q, Liu Z X, et al. Calculation of siphons and minimal siphons in Petri nets based on semi-tensor product of matrices. IEEE Transactions on Systems, Man and Cybernetics: Systems, 2015, DOI: 10.1109/TSMC.2015.2507162

24. Cheng D Z, Qi H S. A linear representation of dynamics of Boolean networks. IEEE Transactions on Automatic Control, 2010, 55(10): 2251-2258

25. Cheng D Z, Qi H S. Controllability and observability of Boolean control networks. Automatica, 2011, 45(7): 1659-1667

26. Guo P L, Wang Y Z, Li T. Algebraic formulation and strategy optimization for a class of evolutionary networked games via semi-tensor product method. Automatica, 2013, 49(11): 3384-3389

27. Xu X R, Hong Y G. Matrix expression and reachability of finite automata. Journal of Control Theory and Applications, 2012, 10(2): 210-215

28. Yan Y Y, Chen Z Q, Liu Z X. Semi-tensor product of matrices approach to reachability of finite automata with application to language recognition. Frontiers of Computer Science, 2014, 8(6): 948-957

29. Yan Y Y, Chen Z Q, Liu Z X. Verification analysis of self-verifying automata via semi-tensor product of matrices. Journal of China Universities of Posts and Telecommunications, 2014, 21(4): 96-104

30. Wang Y Z, Zhang C H, Liu Z B. A matrix approach to graph maximum stable set and coloring problems with application to multi-agent systems. Automatica, 2012, 48(7): 1227-1236

31. Cheng D Z, Qi H S, Zhao Y. An introduction to semi-tensor product of matrices and its applications. Singapore: World Scientific, 2012

32. Yan Y Y, Chen Z Q, Liu Z X. Modelling combined automata via semi-tensor product of matrices. Proceedings of the 33th Chinese Control Conference, Jul 28-30 2014, Nanjing, China. Piscataway, NJ, USA: IEEE, 2014: 6560-6565

33. Buchholz P, Kemper P. Hierarchical reachability graph generation for Petri nets. Formal Methods in System Design, 2010, 21(3): 281-315

Metrics

Comments

Copyright © 2020 The Journal of China Universities of Posts and Telecommunications
　 Adress: P.O. Box 231,Beijing University of Posts and Telecommunications,10 Xi Tucheng Road,Beijing 100876,P.R.China　Post Code: 100081
Tel：86-010-62282493　Fax： 86-010-62283461　E-mail: jchupt@bupt.edu.cn
Support by: Beijing Magtech Co.Ltd

Modeling and reachability analysis of synchronizing transitions bounded Petri net systems based upon semi-tensor product of matrices

PDF

Knowledge

Cited

Abstract

Cite this article

share this article

References

Related Articles 0

Recommended Articles

Metrics

Comments