面向死锁检测与控制的无界Petri网复可达树技术研究

Deadlock detection and control plays an important role in design and operation phase of distributed concurrent systems. Petri net reachability trees are one of the most powerful means for deadlock analysis. However, existing reachability trees can only be applied to some sub-class of Petri nets. To increase the applicable scope of reachability trees in the deadlock control field, the project intends to propose a new type of reachability tree called complex reachability tree, which can be used to detect deadlocks and to design liveness-enforcing supervisors for unbounded Petri nets. The content of this study includes: (1) proposing the construction rules of complex reachability trees dedicated to deadlock detection of unbounded Petri nets, and designing the corresponding construction algorithm; (2) developing the deadlock detection algorithm of unbounded Petri nets based on complex reachability tree, and presenting its corresponding liveness-enforcing supervisor design method; (3) promoting existing Petri net finite complete prefix unfolding techniques from bounded Petri nets to unbounded ones, thereby reducing the analysis difficulty caused by state explosion problem. Based on this project, deadlock detection and control technology is promoted from bounded Petri nets or specific unbounded Petri net classes to a more general classes of unbounded Petri nets, which has significant theoretical value.

死锁检测与控制在分布式并发系统设计与运行中具有重要作用，Petri网可达树是进行死锁分析的主要手段之一。然而，现有可达树仅适用于特定的Petri网子类，本项目拟提出一种应用范围更广、可用于无界Petri网死锁检测与控制的新型可达树—复可达树，并以此为基础研究无界Petri网的死锁检测与活性监督控制器设计技术。研究内容包括：（1）提出面向死锁检测的无界Petri网复可达树构造规则，设计并实现相应的构造算法；（2）以复可达树为基础，给出无界Petri网死锁检测的具体算法，并设计相应的活性监督控制器；（3）将Petri网的有限完全前缀展开技术推广到无界Petri网，以此降低状态爆炸问题给无界Petri网死锁分析带来的困难。通过本项目，将Petri网的死锁检测与控制技术从有界Petri网或特定无界Petri网子类向更为一般的无界Petri网进行推广，这无疑具有重要的理论价值。

Petri网及其可达树是对分布式并发系统进行死锁分析的常见工具，然而，状态爆炸问题阻碍了可达树技术在大规模并发系统实际分析中的应用，与此同时，由于无界系统可达状态的无限性，可达树无法对无界Petri网的死锁进行有效分析。针对上述问题，本项目开展了如下工作：（1）将传统可达树的状态标识推广为由实部标识和虚部标识构成的二元复标识，提出了面向无界Petri网死锁分析的Petri网复可达树的概念，给出了复可达树的构造算法以及基于复可达树的死锁检测方法，证明了复可达树中的任意终端节点都必然对应原无界Petri网的一个死锁标识，复可达树中的任意非终端节点所对应之标识都必然不是死锁，对于无ω-消解节点的Petri网，给出了其存在死锁的充要条件，即一个无ω-消解节点Petri网存在死锁当且仅当其对应的复可达树中存在终端节点；（2）为缓解复可达树存在的、与传统可达树类似的状态爆炸问题，利用出现网与分支进程技术改进复可达树，提出了一种全新的面向死锁检测的无界Petri网展开方法D2U，相比传统的网展开技术，D2U不会出现死锁误警的现象，且对于满足特定条件的一类无界Petri网能对死锁问题作出完整判定；（3）以跨组织协同业务流程管理、并行程序正确性验证为应用背景，将Petri网及其展开等方法应用到了实际系统的智能模型构建与分析中。其中，基于Petri网与流程挖掘的研究方案为多模式复杂业务流程的智能构建与分析、以及并行程序漏洞检测等经典问题提供了新途径。.上述研究内容发表在了Information Sciences、IEEE Transactions on Systems Man Cybernetics-Systems、IEEE Transactions on Services Computing等权威刊物，包括SCI期刊论文7篇，EI论文13篇。授权和申请专利与软件著作权10项。基于Petri网展开的并行程序死锁与数据竞争检测软件获得第七届中国软件杯大赛全国一等奖。研究成果“公共安全物联网与应急联动处置服务平台”、“跨组织多模式协作信息系统的智能感知与性能优化”、“公共安全物联网应急联动平台”分别获得全国商业联合会科技进步二等奖和山东省物联网协会特等奖与一等奖。.上述成果为分布式并发系统的死锁分析提供了新的途径，对于Petri网理论本身也是一种拓展，具有较强的理论和应用价值。