安全Petri网事件分离状态的BDD算法

doi:10.3969/j.issn.1001-2400.2010.01.021

Abstract

Abstract:

Based on the theory of regions, an optimal liveness-enforcing Petri net supervisory can be obtained. However, the set of reachable states is required, which usually leads to the state explosion problem. This paper presents a symbolic approach to the computation of marking/transition separation instances for safe Petri nets by using BDD (Binary Decision Diagrams). In this paper, the structure and behavior of a Petri net are symbolically modeled by using Boolean algebra. Boolean algebra operations are implemented by BDD which are capable of representing large sets of reachable states with small shared data structures and enable the efficient manipulation of those sets. Therefore, the cost of computation and memory usage can be efficiently reduced. Finally, using the model of the well-known dining philosophers problem, we verify the efficiency of calculating the set of legal states, dangerous states, bad states and the marking/transition separation instances through different-sized problems.

Key words: Petri nets, binary decision diagrams(BDD), marking/transition separation instances

CHEN Yu-feng;LI Zhi-wu. Computation of marking/transition separation instances for safe Petri nets using BDD[J].J4, 2010, 37(1): 119-124+141.

References

［1］Ezpeleta J, Colom J M, Martinez J. A Petri Net Based Deadlock Prevention Policy for Flexible Manufacturing Systems［J］. IEEE Trans on Robotics and Automation, 1995, 11(2): 173-184.
［2］Li Zhiwu, Zhou Mengchu. Elementary Siphons of Petri Nets and Their Application to Deadlock Prevention in Flexible Manufacturing Systems［J］. IEEE Trans on Systems, Man, and Cybernetics, Part A, 2004, 34(1): 38-51.
［3］Li Zhiwu, Zhou Mengchu. Clarifications on the Definitions of Elementary Siphons of Petri Nets［J］. IEEE Trans on Systems, Man, and Cybernetics, Part A, 2006, 36(6): 1227-1229.
［4］Li Zhiwu, Hu Hesuan, Wang Anrong. Design of Liveness-enforcing Supervisors for Flexible Manufacturing Systems Using Petri nets［J］. IEEE Trans on Systems, Man, and Cybernetics, Part C, 2007, 37(4): 517-526.
［5］Li Zhiwu, Zhou Mengchu. Two-stage Method for Synthesizing Liveness-enforcing Supervisors for Flexible Manufacturing Systems Using Petri Nets［J］. IEEE Trans on Industrial Informatics, 2006, 2(4): 313-325.
［6］闫明明, 李志武, 钟春富. S³PR网的一种死锁预防策略［J］. 西安电子科技大学学报, 2008, 35(2), 330-333.
Yan Mingming, Li Zhiwu, Zhong Chunfu. Deadlock Prevention Policy for a Class of Petri Nets S³PR［J］. Journal of Xidian University, 2008, 35(2): 330-333.
［7］Ghaffari A, Rezg N, Xie X L. Design of a Live and Maximally Permissive Petri Net Controller Using the Theory of Regions［J］. IEEE Trans on Robotics and Automation, 2003, 19(1): 137-142.
［8］Pastor E, Cortadella J, Roig O, et al. Petri Net Analysis Using Boolean Manipulation［C］//Lecture Notes in Computer Science: 815. London: Springer-Verlag, 1994: 416-435.
［9］Pastor E, Cortadella J. Symbolic Analysis of Bounded Petri Nets［J］. IEEE Trans on Computers, 2001, 50(5), 432-448.
［10］Miner A S, Ciardo G. Efficient Reachability Set Generation and Storage Using Decision Diagrams［C］//Lecture Notes in Computer Science: 1639. London: Springer-Verlag, 1999: 6-25.
［11］Andersen H R. An Introduction to Binary Decision Diagrams［R］. Denmark: Advanced Algorithms E97, Department of Information Technology, Technical University of Denmark, 1997.
［12］Brant R E. Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams［J］. ACM Computing Surveys, 1992, 24(3): 293-318.

[1]	WANG Qi;CHEN Xiaoliang. Algorithm for estimating confusion states of flexible manufacturing systems [J]. Journal of Xidian University, 2017, 44(2): 69-74.
[2]	JIANG Zhongyuan;ZHANG Xiuyan;MA Ziyue. Capacity optimization for power storage systems in smart grids [J]. J4, 2015, 42(6): 106-112.
[3]	ZHANG Xiuyan;ZHONG Chunfu;JIA Jianyuan. Method to compute the reachability set of S³PR [J]. J4, 2015, 42(5): 105-109.
[4]	ZHANG Li;ZHAO Liangxu;WANG Shouguang;WANG Chengying. Optimal linear constraint transformation method for α-nets [J]. J4, 2015, 42(5): 183-187+212.
[5]	CHEN Xiaoliang;JIANG Zhongyuan;YE Jianhong . Confusion detection and prevention policies for workflow nets [J]. J4, 2015, 42(2): 77-83.
[6]	ZHU Chengcheng;DONG Lida. Concurrency bug test for a class of multithreaded software [J]. J4, 2015, 42(2): 167-173+212.
[7]	LI Ye;WANG Yinghui;YU Zhenhua. Formal modeling of cyber-physical systems using object-oriented Petri nets [J]. J4, 2014, 41(2): 165-171.
[8]	WANG Qi;WANG Anrong;PU Xuqiang. Computation of special markings of Petri nets of manufacturing systems [J]. J4, 2013, 40(6): 85-91.
[9]	. Deadlock prevention approach for a class of timed Petri nets [J]. J4, 2009, 36(5): 902-908.
[10]	ZHU Sen;LI Zhi-wu. On the colored Petri net model of the C³I system of the double aircraft carriers group [J]. J4, 2009, 36(4): 661-668.
[11]	WANG An-rong;DUAN Jiang-tao;LI Zhi-wu;JIA Jian-yuan. On the forbidden state avoidance of resource allocation systems [J]. J4, 2005, 32(5): 742-747.
[12]	MA Yu-xiang;LI Yuan-jun;LIU Yan-ming. A modeling and verification method for ingtelligent networks services with Petri nets [J]. J4, 2004, 31(2): 194-198.
[13]	LI Zhi-wu;WANG An-rong;JIA Jian-yuan. Methods for solving invariants and state equations for Petri nets [J]. J4, 2003, 30(2): 259-263.

Computation of marking/transition separation instances for safe Petri nets using BDD

PDF (PC)

Like

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 13

Metrics

Comments

Recommended 10