A journal of IEEE and CAA , publishes high-quality papers in English on original theoretical/experimental research and development in all areas of automation
Volume 6 Issue 3
May  2019

IEEE/CAA Journal of Automatica Sinica

• JCR Impact Factor: 6.171, Top 11% (SCI Q1)
CiteScore: 11.2, Top 5% (Q1)
Google Scholar h5-index: 51， TOP 8
Turn off MathJax
Article Contents
Dmitry A. Zaitsev, Tatiana R. Shmeleva and Jan Friso Groote, "Verification of Hypertorus Communication Grids by Infinite Petri Nets and Process Algebra," IEEE/CAA J. Autom. Sinica, vol. 6, no. 3, pp. 733-742, May 2019. doi: 10.1109/JAS.2019.1911486
 Citation: Dmitry A. Zaitsev, Tatiana R. Shmeleva and Jan Friso Groote, "Verification of Hypertorus Communication Grids by Infinite Petri Nets and Process Algebra," IEEE/CAA J. Autom. Sinica, vol. 6, no. 3, pp. 733-742, May 2019.

# Verification of Hypertorus Communication Grids by Infinite Petri Nets and Process Algebra

##### doi: 10.1109/JAS.2019.1911486
Funds:  This work was supported in part by NATO(ICS.NUKR.CLG982689)
• A model of a hypertorus communication grid has been constructed in the form of an infinite Petri net. A grid cell represents either a packet switching device or a bioplast cell. A parametric expression is obtained to allow a finite specification of an infinite Petri net. To prove properties of an ideal communication protocol, we derive an infinite Diophantine system of equations from it, which is subsequently solved. Then we present the programs htgen and ht-mcrl2-gen, developed in the C language, which generate Petri net and process algebra models of a hypertorus with a given number of dimensions and grid size. These are the inputs for the respective modeling tools Tina and mCRL2, which provide model visualization, step simulation, state space generation and reduction, and structural analysis techniques. Benchmarks to compare the two approaches are obtained. An ad-hoc induction-like technique on invariants, obtained for a series of generated models, allows the calculation of a solution of the Diophantine system in a parametric form. It is proven that the basic solutions of the infinite system have been found and that the infinite Petri net is bounded and conservative. Some remarks regarding liveness and liveness enforcing techniques are also presented.

•  [1] D. A. Zaitsev, I. D. Zaitsev, and T. R. Shmeleva, "Infinite petri nets: part 1, modeling square grid structures, " Complex Systems, vol. 26, no. 2, pp. 157-195, 2017. [2] D. A. Zaitsev, I. D. Zaitsev and T. R. Shmeleva, "Infinite petri nets: part 2, modeling square grid structures, " Complex Systems, vol. 26, no. 4, pp. 341-371, 2017. [3] D. A. Zaitsev and T. R. Shmeleva, "Verification of hypercube communication structures via parametric Petri nets, " Cybernetics and Systems Analysis, vol. 46, no. 1, pp. 105-114, 2010. [4] D. A. Zaitsev, "Verification of computing grids with special edge conditions by infinite petri nets, " Automatic Control and Computer Sciences, vol. 47, no. 7, pp. 403-412, 2013. [5] T. R. Shmeleva, D. A. Zaitsev, and I. D. Zaitsev, "Verification of square communication grid protocols via infinite Petri nets, " in Proc. of MESM 10th Middle Eastern Simulation Multiconference, 2009, 53-59. [6] S. Cheng, W. Zhong, and K. E. Isaacs, and K. Mueller, "Visualizing the topology and data traffic of multi-dimensional torus interconnect networks, " IEEE Access, 2018. [7] N. P. Preve (Ed.), Grid Computing: Towards a Global Interconnected Infrastructure, Springer, 2011. [8] D. Gilbert, M. Heiner, F. Liu, and N. Saunders, "Colouring space - a coloured framework for spatial modelling in systems biology, " in Proc. Conf. Petri Nets, Milano, Springer, LNCS, vol. 7927, pp. 230-249, June 2013. [9] K. Miyamoto, Plasma Physics and Controlled Nuclear Fusion. Springer, 2005. [10] L. V. Belevtsov and A. A. Kostikov, "Influence of grain properties on the Abrikosov vortices interaction with Josephson junction, " Journal of Low Temperature Physics, vol. 139, no. 1, pp. 11-19, 2005. http://www.wanfangdata.com.cn/details/detail.do?_type=perio&id=9a05b5a41cf3fd4db3a66eec0fa213d3 [11] B. Berthomieu, O.-P. Ribet, and F. Vernadat, "The tool TINA-construction of abstract state space for Petri nets and time Petri nets, " Int. J. Prod. Res., vol. 42, no. 14, pp. 2741-2756, 2004. [12] B. Berthomieu et al., "Tina: Time Petri Net Analyser, " LAAS, 2019 [Online]. Available: http:/projects.laas/fr/tina [13] D. A. Zaitsev, "Software of Dmitry Zaitsev, " GitHub, 2019 [Online]. Available: https://github.com/dazeorgacm/ [14] J. F. Groote and M. R. Mousavi. Modeling and Analysis of Communicating Systems. The MIT Press, 2014. [15] J. F. Groote et al, "mCRL2: Analysing System Behaviour, " TU/e, 2019.[Online]. Available: https://www.mcrl2.org/ [16] T. A. N. Engels, J. F. Groote, M. J. van Weerdenburg, and T. A. C. Willemse, "Search algorithms for automated validation, " Journal of Logic and Algebraic Programming, vol. 78, no. 4, pp. 274-287, 2009. [17] D. A. Zaitsev, "A generalized neighborhood for cellular automata, " Theoretical Computer Science, vol. 666, pp. 21-35, March 2017. [18] G. Berthelot and R. Terrat, "Petri nets theory for the correctness of protocols, " IEEE Trans. on Communications, vol. 30, no. 12, pp. 2497-2505, 1982. [19] M. Diaz, "Modelling and analysis of communication and cooperation protocols using petri net based model, " Computer Networks, no. 6. pp. 419-441, 1982. [20] T. Murata, "Petri Nets: Properties, Analysis and Applications, " Proc. of the IEEE, vol. 77, no. 4, pp. 541-580, 1989. doi: 10.1109/5.24143 [21] Z. W. Li and M. C. Zhou, Deadlock Resolution in Automated Manufacturing Systems, Springer, 2010. [22] D. A. Zaitsev, "Decomposition of petri nets, " Cybernetics and Systems Analysis, vol. 40, no. 5, pp. 739-746, 2004. [23] J. Ye, M. C. Zhou, Z. Li, and A. Al-Ahmari, "Structural Decomposition and Decentralized Control of Petri Nets, " IEEE Transactions on Systems, Man, and Cybernetics: Systems, pp. 1-10, DOI: 10.1109/TSMC.2017.2703950,July2017. [24] D. A. Zaitsev and A. I. Sleptsov, "State Equations and Equivalent Transformation for Timed Petri Nets, " Cybernetics and Systems Analysis, vol. 33, no. 5, pp. 659-672, 1997. [25] J. Luo, H. Ni, W. Wu, S. Wang, and M. C. Zhou, "Simultaneous reduction of petri nets and linear constraints for efficient supervisor synthesis, " IEEE Trans. on Automatic Control, vol. 60, no. 1, pp. 88-103, Jan. 2015. [26] N. Wu, M. C. Zhou, and G. Hu, "Petri net modeling and one-step look-ahead maximally permissive deadlock control of automated manufacturing systems, " ACM Transactions on Embedded Computing Systems, vol. 12, no. 1, pp. 10: 1-10: 23, Jan. 2013. [27] H. Liu, K. Xing, W. Wu, M. C. Zhou, and H. Zou, "Deadlock prevention for flexible manufacturing systems via controllable siphon basis of petri nets, " IEEE Trans. Systems, Man, and Cybernetics: Systems, vol. 45, no. 3, pp. 519-529, Mar. 2015. [28] D. You, S. Wang, and M. C. Zhou, "Synthesis of monitor-based liveness-enforcing supervisors for S3PR with $xi$-resources, " IEEE Trans. Systems, Man, and Cybernetics: Systems, vol. 45, no. 6, pp. 967-975, June 2015. [29] H. Chen, N. Wu, and M. C. Zhou, "A novel method for deadlock prevention of AMS by using resource-oriented petri nets, " Information Sciences, vol. 363, pp. 178-189, Oct. 2016. [30] D. A. Zaitsev, T. R. Shmeleva, W. Retschitzegger, and B. Proll, "Security of grid structures under disguised traffic attacks, " Cluster Computing, vol. 19, no. 3, pp. 1183-1200, 2016. [31] F. Kordon et al., "Model Checking Contest, " Sorbonne, 2019 [Online]. Available: https://mcc.lip6.fr

### Catalog

###### 通讯作者: 陈斌, bchen63@163.com
• 1.

沈阳化工大学材料科学与工程学院 沈阳 110142

Figures(8)  / Tables(2)

## Article Metrics

Article views (1362) PDF downloads(35) Cited by()

/