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

被引:0
作者
Chen Y.-F. [1 ]
Li Z.-W. [1 ]
机构
[1] School of Mechano-electronic Engineering, Xidian Univ.
来源
Xi'an Dianzi Keji Daxue Xuebao/Journal of Xidian University | 2010年 / 37卷 / 01期
关键词
Binary decision diagrams(BDD); Marking/transition separation instances; Petri nets;
D O I
10.3969/j.issn.1001-2400.2010.01.021
中图分类号
学科分类号
摘要
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.
引用
收藏
页码:119 / 124+141
相关论文
共 12 条
  • [1] Ezpeleta J., Colom J.M., Martinez J., A petri net based deadlock prevention policy for flexible manufacturing systems, IEEE Trans on Robotics and Automation, 11, 2, pp. 173-184, (1995)
  • [2] Li Z., Zhou M., Elementary siphons of petri nets and their application to deadlock prevention in flexible manufacturing systems, IEEE Trans on Systems, Man, and Cybernetics, Part A, 34, 1, pp. 38-51, (2004)
  • [3] Li Z., Zhou M., Clarifications on the definitions of elementary siphons of petri nets, IEEE Trans on Systems, Man, and Cybernetics, Part A, 36, 6, pp. 1227-1229, (2006)
  • [4] Li Z., Hu H., Wang A., Design of liveness-enforcing supervisors for flexible manufacturing systems using petri nets, IEEE Trans on Systems, Man, and Cybernetics, Part C, 37, 4, pp. 517-526, (2007)
  • [5] Li Z., Zhou M., Two-stage method for synthesizing liveness-enforcing supervisors for flexible manufacturing systems using petri nets, IEEE Trans on Industrial Informatics, 2, 4, pp. 313-325, (2006)
  • [6] Yan M., Li Z., Zhong C., Deadlock prevention policy for a class of petri nets S<sup>3</sup>PR, Journal of Xidian University, 35, 2, pp. 330-333, (2008)
  • [7] Ghaffari A., Rezg N., Xie X.L., Design of a Live and maximally permissive petri net controller using the theory of regions, IEEE Trans on Robotics and Automation, 19, 1, pp. 137-142, (2003)
  • [8] Pastor E., Cortadella J., Roig O., Et al., Petri Net analysis using boolean manipulation, Lecture Notes in Computer Science: 815, pp. 416-435, (1994)
  • [9] Pastor E., Cortadella J., Symbolic analysis of bounded petri nets, IEEE Trans on Computers, 50, 5, pp. 432-448, (2001)
  • [10] Miner A.S., Ciardo G., Efficient reachability set generation and storage using decision diagrams, Lecture Notes in Computer Science: 1639, pp. 6-25, (1999)