中文摘要：

Petri网是一种适合于并发系统建模、分析和控制的图形工具.可达树是Petri网分析的典型技术之一,它通过标识向量集合表征系统的状态空间,组合复杂性严重制约了该分析技术可处理系统问题的规模.零压缩决策图（Zero-Suppressed Binary Decision Diagrams,ZBDD）是一种新型的数据结构,是表示和处理稀疏向量集合的一种有效技术.文章基于Petri网可达标识向量的稀疏特征,给出了Petri网分析的符号ZBDD技术,该技术通过对标识向量（状态）的布尔向量表示、可达标识向量（状态）的符号ZBDD生成,实现Petri网可达状态空间的高效符号操作和紧凑符号表示.实验表明,基于ZBDD的符号可达性分析算法能够有效处理较大规模Petri网问题.

英文摘要：

Petri net is a graph-based mathematical formalism suitable to model, analyze and control the behavior of discrete event concurrent systems. Reachability tree is one of typical techniques to analyze Petri nets. Highly concurrent systems often suffer from state combinatorial explosion problem which renders it very hard and even impossible to handle Petri nets using the reachability tree technique. Fortunately, the marking vectors or the state spaces of Petri nets are often very sparse, and Zero-Suppressed Binary Decision Diagram （ZBDD） is a novel data structure and efficient way to represent and manipulate 0-1 sparse vectors. The authors developed the novel ZBDD-based symbolic technique to formulate, generated and manipulated the reachability marking vectors,thus the performance of Petri nets could be evaluated symbolically. The experimental results show that the symbolic technique can handle large-scale Petri nets more efficiently and compactly.