中文摘要：

基于区域法可以获得最佳的活性控制器，但由于要计算网的可达状态集而导致状态爆炸问题．提出一种应用二值决策图（BDD）计算安全Petri网事件分离状态的算法．用布尔代数对Petri网的结构和行为进行描述，用BDD实现布尔代数运算．BDD共享的数据结构能以较小的空间表示较大可达集并能对其进行高效的运算，从而节省了存储空间，减少了运算时间．最后用著名的哲学家就餐问题的Petri网模型对该算法进行仿真．仿真结果说明，使用BDD计算复杂Petri网的合法状态集、危险节点、坏点和计算事件分离状态具有很高效率．

英文摘要：

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.