无界Petri网分析理论与方法

The analysis of unbounded Petri nets remains one of the most difficult problems in the fields of discrete event systems and Petri nets. To date, there are still many issues to be resolved, such as the inaccuracy of information representation with the existing finite reachability trees; the lack of liveness, deadlock, and reachability analysis methods for generalized unbounded nets (GUNs), and applications of these modeling and analysis methods. To solve these issues, this proposal intends to present: (1) Two novel types of finite reachability trees called type-I and II ones (or I/II-FRT for short) and their generation algorithms that can remove the fake markings during their generation to ensure the accuracy of information representation; (2) An I-FRT-based deadlock analysis method for a class of ω-independent GUNs and II-FRT-based method for liveness and deadlock analysis of ordinary unbounded nets and GUNs, breaking the existing limit to 1-place-unbounded nets; (3) A strategy and method for adaptive finite growth of II-FRTs and their incremental analysis by using cloud computing and cloud storage technologies and a practical method for general reachability analysis of GUNs; and (4) novel application of the unbounded net modeling and analysis methods to the analysis and verification of reactive software. This research is expected to promote the study of unbounded net analysis and the final solution for this long-standing open problem, and to provide theoretical support for the related applications. It is of great theoretical meaning and considerable application values.

无界Petri网分析问题一直是离散事件系统和Petri网领域的世界性研究难题之一，现有研究存在的问题与不足包括：有限可达树信息表示的不准确，缺乏广义无界网活性、死锁及可达性分析方法，以及缺乏应用研究。本申请项目拟提出两种新型的I型和II型有限可达树（I/II-FRT）及生成算法，可在树生成时去除虚假标识信息，确保网状态表示的准确性；基于I-FRT提出一类ω无关广义无界网的死锁分析方法和基于II-FRT的平凡无界网与广义无界网的活性、死锁分析方法，突破现有研究对象仅限于1-库所无界网的局面；提出II-FRT的自适应有限生长与增量式分析策略与方法，结合云计算与云存储技术，建立广义无界网的一般可达性分析的实用化方法；展开无界网在反应式软件的建模、分析与验证中的应用研究。研究有望推动无界网分析问题的研究与最终解决，为相关应用提供建模理论与分析方法，具有重大的理论与一定的应用价值。

无界Petri 网分析问题是离散事件系统和Petri 网领域的世界性研究难题之一，现有研究存在的问题与不足包括：有限可达树信息表示的不准确，缺乏广义无界网活性、死锁及可达性分析方法，以及缺乏应用研究。本申请项目提出了两种新型的I 型和II型有限可达树（I/II-FRT）及生成算法，可在树生成时去除虚假标识信息，确保网状态表示的准确性；基于I-FRT 提出了一类ω无关广义无界网的死锁分析方法和基于II-FRT 的平凡无界网与广义无界网的活性、死锁分析方法，突破了现有研究对象仅限于1-库所无界网的局面；提出了II-FRT 的自适应有限生长与增量式分析策略与方法，结合云计算与云存储技术，建立了广义无界网的一般可达性分析的实用化方法；开展了无界网在反应式软件的建模、分析与验证中的应用研究。该项目推动了无界网分析问题的研究与发展，为相关应用提供了建模理论与分析方法，具有重大的理论与一定的应用价值。