logo

SCIENCE CHINA Information Sciences, Volume 61, Issue 1: 010205(2018) https://doi.org/10.1007/s11432-017-9283-7

Modeling and analysis of colored petri net based on the semi-tensor product of matrices

More info
  • ReceivedAug 18, 2017
  • AcceptedSep 28, 2017
  • PublishedDec 11, 2017

Abstract

This paper applies the model petri net method based on the semi-tensor product of matrices to colored petri net. Firstly, we establish the marking evolution equation for colored petri net by using the semi-tensor product of matrices. Then we define the concept of controllability and the control-marking adjacency matrix for colored petri net. Based on the marking evolution equation and control-marking adjacency matrix, we give the necessary and sufficient condition of reachability and controllability for colored petri net. The algorithm to verify the reachability of colored petri net is given, and we analyze the computational complexity of the algorithm. Finally, an example is given to illustrate the effectiveness of the proposed theory. The significance of the paper lies in the application of the model petri net method based on the semi-tensor product of matrices to colored petri net. This is a convenient way of verifying whether one marking is reachable from another one as well as finding all firing sequences between any two reachable markings. Additionally, the method lays the foundations for the analysis of other properties of colored petri net.


Acknowledgment

This work was supported by National Natural Science Foundation of China (Grant Nos. 61573199, 61573200), Tianjin Natural Science Foundation of China (Grant Nos. 14JCYBJC18700, 13JCYBJC17400).


References

[1] Billington J, Gallasch G E, Han B. A coloured petri net approach to protocol verification. In: Lectures on Concurrency and Petri Nets. Berlin: Springer, 2004. Google Scholar

[2] Saitou K, Malpathak S, Qvam H. Robust design of flexible manufacturing systems using, colored petri net and genetic algorithm. J Intell Manuf, 2002, 13: 339--351. Google Scholar

[3] Ezpeleta J, Colom J M. Automatic synthesis of colored petri nets for the control of FMS. IEEE Trans Robot Autom, 1997, 13: 327--337. Google Scholar

[4] Shapiro R M. Validation of a VLSI chip using hierarchical colored petri nets. In: High-level Petri Nets. Berlin: Springer, 1991. 607--625. Google Scholar

[5] Viswanadham N, Narahari Y. Coloured petri net models for automated manufacturing systems. In: Proceedings of IEEE International Conference on Robotics and Automation, Raleigh, 1987. Google Scholar

[6] Jensen K. Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use, Volume 1, Basic Concepts. Berlin: Springer, 1992. Google Scholar

[7] Jensen K. Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use, Volume 2, Analysis Methods. Berlin: Springer, 1997. Google Scholar

[8] Jensen K. Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use, Volume 3. Berlin: Springer, 1997. Google Scholar

[9] Ding Z H, Jiang M Y, Chen H B, et al. Petri net based test case generation for evolved specification. Sci China Inf Sci, 2016, 59: 080105. Google Scholar

[10] Cheng D Z. Semi-tensor product of matrices and its application to Morgens problem. Sci China Ser F-Inf Sci, 2001, 44: 195--212. Google Scholar

[11] Cheng D Z, Qi H S, Li Z Q. Controllability and observability of boolean control networks. In: Analysis and Control of Boolean Networks. Berlin: Springer, 2011. 213--231. Google Scholar

[12] Cheng D Z, Qi H S. A linear representation of dynamics of Boolean networks. IEEE Trans Autom Control, 2010, 55: 2251--2258. Google Scholar

[13] Cheng D Z. Disturbance decoupling of Boolean control networks. IEEE Trans Autom Control, 2011, 56: 2--10. Google Scholar

[14] Li H T, Wang Y Z, Guo P L. Output reachability analysis and output regulation control design of Boolean control networks. Sci China Inf Sci, 2017, 60: 022202. Google Scholar

[15] Chen H W, Liang J L, Wang Z D. Pinning controllability of autonomous Boolean control networks. Sci China Inf Sci, 2016, 59: 070107. Google Scholar

[16] Liu R J, Lu J Q, Liu Y, et al. Delayed feedback control for stabilization of Boolean control networks with state delay. IEEE Trans Neural Netw Learn Syst, 2017, 99: 1--6. Google Scholar

[17] Chen H W, Liang J L, Lu J Q. Partial synchronization of interconnected Boolean networks. IEEE Trans Cybern, 2016, 47: 258--266. Google Scholar

[18] Liu Y, Chen H W, Lu J Q, et al. Controllability of probabilistic Boolean control networks based on transition probability matrices. Automatica, 2015, 52: 340--345. Google Scholar

[19] Zhang K Z, Zhang L J. Controllability of probabilistic Boolean control networks with time-variant delays in states. Sci China Inf Sci, 2016, 59: 092204. Google Scholar

[20] Guo Y Q. Controllability of Boolean control networks with state-dependent constraints. Sci China Inf Sci, 2016, 59: 032202. Google Scholar

[21] Xu X R, Hong Y G. Matrix expression and reachability analysis of finite automata. J Control Theory Appl, 2012, 10: 210--215. Google Scholar

[22] Xu X R, Hong Y G. Observability analysis and observer design for finite automata via matrix approach. IET Control Theory Appl, 2013, 7: 1609--1615. Google Scholar

[23] Cheng D Z. On finite potential games. Automatica, 2014, 50: 1793--1801. Google Scholar

[24] Cheng D Z, He F H, Qi H S, et al. Modeling, analysis and control of networked evolutionary games. IEEE Trans Autom Control, 2015, 60: 2402--2415. Google Scholar

[25] Guo P L, Wang Y Z, Li H T. Stable degree analysis for strategy profiles of evolutionary networked games. Sci China Inf Sci, 2016, 59: 052204. Google Scholar

[26] Wang Y Z, Cheng D Z. Dynamics and stability for a class of evolutionary games with time delays in strategies. Sci China Inf Sci, 2016, 59: 092209. Google Scholar

[27] Yan Y Y, Chen Z Q, Liu Z X. Solving type-2 fuzzy relation equations via semi-tensor product of matrices. Control Theory Technol, 2014, 12: 173--186. Google Scholar

[28] 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 Trans Syst Man Cybern Syst, 2017, 47: 531--536. Google Scholar

[29] 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. In: Proceedings of the 34th Chinese Control Conferences, Hangzhou, 2015. 6586--6591. Google Scholar

[30] Yan Y Y, Chen Z Q, Yue J M, et al. STP approach to model controlled automata with application to reachability analysis of DEDS. Asian J Control, 2016, 18: 2027--2036. Google Scholar

[31] Gradshteyn I S, Ryzhik I M, Romer R H. Tables of integrals, series, and products. Am J Phys, 1988, 56: 958. Google Scholar

  • Figure 1

    The colored petri net of dining philosophers.

  • Figure 2

    The state space of the colored petri net of dining philosophers.

  • Figure 3

    The colored petri net used to verify the reachability and controllability.

  • Figure 4

    The state space of the colored petri net used to verify the reachability and controllability.

  •   

    Algorithm 1 Verifying the reachability of colored petri net

    Consider a colored petri net $\langle~{\rm~CPN},M_{1}~\rangle$ with $m$ transitions, $n$ variables, and $s$ markings, and where $M_{i}=\delta_{s}^{i}$ and $M_{j}=\delta_{s}^{j}$ are two markings. We can verify whether $M_{j}$ is reachable from $M_{i}$ by $t$ steps by the following method. Step 1: Construct the marking evolution equation of $\langle~{\rm~CPN},M_{1}~\rangle$. Step 2: Calculate the matrix $(LW_{[s,mh]})^{t}\delta_{s}^{i}$. If $\delta_{s}^{j}\notin~{\rm~Col}((LW_{[s,mh]})^{t}\delta_{s}^{i})$ then $\delta_{s}^{j}$ is not reachable from $\delta_{s}^{i}$ in $t$ steps. Step 3: Find all $k$ such that $\delta_{s}^{j}={\rm~Col}_{k}((LW_{[s,mh]})^{t}\delta_{s}^{i})$. Now $\delta_{(mh)^{t}}^{k}=\ltimes_{j=1}^{t}\delta_{mh}^{k_{j}}$ and we can obtain $k_j$, $(j=1,2,\ldots,t)$ by decomposing the semi-tensor product of matrices. Thus, we can find the firing sequence $\delta_{mh}^{k_{1}}$,$\delta_{mh}^{k_{2}}$,$\delta_{mh}^{k_{3}}$,…,$\delta_{mh}^{k_{t}}$. For each $\delta_{mh}^{k_{j}},(j=1,2,\ldots,t)$, we can also obtain the firing transition and the binding for all variables by decomposing the semi-tensor product of matrices.

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

京ICP备18024590号-1       京公网安备11010102003388号